Merge pull request #3413 from mtzguido/imp_refactor

Refactoring implicit instantiation
FStarLang · Aug 26, 2024 · a26252e · a26252e
2 parents 04413e8 + 0ab882f
commit a26252e
Show file tree

Hide file tree

Showing 10 changed files with 304 additions and 392 deletions.
diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Subst.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Subst.ml
diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml
diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml
diff --git a/src/syntax/FStar.Syntax.Subst.fst b/src/syntax/FStar.Syntax.Subst.fst
@@ -294,6 +294,7 @@ let subst_binder' s b =
     b.binder_positivity
     (b.binder_attrs |> List.map (subst' s))
 
+let subst_binder s (b:binder) = subst_binder' ([s], NoUseRange) b
 
 let subst_binders' s bs =
     bs |> List.mapi (fun i b ->

diff --git a/src/syntax/FStar.Syntax.Subst.fsti b/src/syntax/FStar.Syntax.Subst.fsti
@@ -31,6 +31,7 @@ val subst_aqual:        list subst_elt -> aqual -> aqual
 val subst_ascription:   list subst_elt -> ascription -> ascription
 val subst_decreasing_order:
                         list subst_elt -> decreases_order -> decreases_order
+val subst_binder:       list subst_elt -> binder -> binder
 val subst_binders:      list subst_elt -> binders -> binders
 val subst_residual_comp:list subst_elt -> residual_comp -> residual_comp
 val compress:           term -> term