Merge pull request #3607 from FStarLang/_nik_490_revisited

Substitution must be fully applied in extraction
FStarLang · Nov 7, 2024 · e1d9990 · e1d9990
2 parents 37eca61 + 35dc462
commit e1d9990
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 3 deletions.
diff --git a/ocaml/fstar-lib/generated/FStarC_Extraction_ML_Modul.ml b/ocaml/fstar-lib/generated/FStarC_Extraction_ML_Modul.ml
diff --git a/src/extraction/FStarC.Extraction.ML.Modul.fst b/src/extraction/FStarC.Extraction.ML.Modul.fst
@@ -360,8 +360,8 @@ let extract_typ_abbrev env quals attrs lb
         in
         tcenv, as_pair def_typ
     in
-    let lbtyp = FStarC.TypeChecker.Normalize.normalize [Env.Beta;Env.UnfoldUntil delta_constant; Env.ForExtraction] tcenv lbtyp in
-    //eta expansion is important; see issue #490
+    let lbtyp = FStarC.TypeChecker.Normalize.normalize [Env.Beta;Env.UnfoldUntil delta_constant; Env.ForExtraction; Env.Unrefine; Env.Unascribe ] tcenv lbtyp in
+    //eta expansion is important; see issue #490, including unrefining and unascribing
     let lbdef = FStarC.TypeChecker.Normalize.eta_expand_with_type tcenv lbdef lbtyp in
     let fv = right lb.lbname in
     let lid = fv.fv_name.v in