Merge pull request #3556 from mtzguido/move

ulib: move a type into stubs
FStarLang · Oct 10, 2024 · 9ec5695 · 9ec5695
2 parents 59f13d3 + 724725e
commit 9ec5695
Show file tree

Hide file tree

Showing 6 changed files with 16 additions and 16 deletions.
diff --git a/ocaml/fstar-lib/generated/FStar_Reflection_TermEq.ml b/ocaml/fstar-lib/generated/FStar_Reflection_TermEq.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Reflection_Typing.ml b/ocaml/fstar-lib/generated/FStar_Reflection_Typing.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_NamedView.ml b/ocaml/fstar-lib/generated/FStar_Tactics_NamedView.ml
diff --git a/ulib/FStar.Stubs.Reflection.Types.fsti b/ulib/FStar.Stubs.Reflection.Types.fsti
@@ -40,11 +40,4 @@ type univ_name = ident
 type typ     = term
 type binders = list binder
 
-(*
- * match e as binder returns t|C
- *
- * the bool says whether returns (bool = false) or returns$ (bool = true, use type equality
- *)
-type match_returns_ascription = binder & (either term comp & option term & bool)
-
 type decls = list sigelt
diff --git a/ulib/FStar.Stubs.Reflection.V1.Data.fsti b/ulib/FStar.Stubs.Reflection.V1.Data.fsti
@@ -22,6 +22,7 @@ open FStar.Stubs.Reflection.V2.Data {}
 open FStar.Stubs.Reflection.V2.Builtins {}
 
 open FStar.Stubs.Reflection.Types
+open FStar.Stubs.Syntax.Syntax
 
 (* V1 does not really use the primitive ident type, but this
 explicit pair of string & range *)

diff --git a/ulib/FStar.Stubs.Syntax.Syntax.fsti b/ulib/FStar.Stubs.Syntax.Syntax.fsti
@@ -10,3 +10,11 @@ type subst_elt =
   | UN : int -> universe -> subst_elt
   | UD : ident -> int -> subst_elt
 type subst_t = list subst_elt
+
+
+(*
+ * match e as binder returns t|C
+ *
+ * the bool says whether returns (bool = false) or returns$ (bool = true, use type equality
+ *)
+type match_returns_ascription = binder & (either term comp & option term & bool)