Fix exposed definition of ident (FStarLang#2444)

W95Psp · Feb 14, 2022 · 699c5ce · 699c5ce
1 parent 727fcfc
commit 699c5ce
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 1 deletion.
diff --git a/CHANGES.md b/CHANGES.md
@@ -367,6 +367,10 @@ Guidelines for the changelog:
 
 ## Miscellaneous
 
+   * [Issue #2444](https://github.com/FStarLang/FStar/issues/2444) The
+     definition of the type `ident` exposed `FStar.Reflection.Types`
+     is now `string * range` instead of `range * string`.
+
    * Development builds of F\* no longer report the date of the build
      in `fstar --version`. This is to prevent needlessly rebuilding
      F\* even when the code does not change.

diff --git a/ulib/FStar.Reflection.Types.fsti b/ulib/FStar.Reflection.Types.fsti
@@ -28,7 +28,8 @@ assume new type ctx_uvar_and_subst
 assume new type letbinding
 
 type name : eqtype = list string
-type ident = range * string
+type ident = string * range
 type univ_name = ident
 type typ     = term
 type binders = list binder
+