Merge pull request #3242 from mtzguido/reals

Making Reals erasable, and providing a reflection API for real literals
FStarLang · Apr 18, 2024 · e95e387 · e95e387
2 parents a80d03c + 060ceeb
commit e95e387
Show file tree

Hide file tree

Showing 26 changed files with 405 additions and 205 deletions.
diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Util.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Util.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Parser_Const.ml b/ocaml/fstar-lib/generated/FStar_Parser_Const.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml b/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Real_Old.ml b/ocaml/fstar-lib/generated/FStar_Real_Old.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Reflection_V2_Builtins.ml b/ocaml/fstar-lib/generated/FStar_Reflection_V2_Builtins.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Reflection_V2_Compare.ml b/ocaml/fstar-lib/generated/FStar_Reflection_V2_Compare.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Reflection_V2_Data.ml b/ocaml/fstar-lib/generated/FStar_Reflection_V2_Data.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Reflection_V2_TermEq.ml b/ocaml/fstar-lib/generated/FStar_Reflection_V2_TermEq.ml