Subst has been added to the kernel.

[helm.git] / helm / ocaml / cic_unification / cicMkImplicit.ml

diff --git a/helm/ocaml/cic_unification/cicMkImplicit.ml b/helm/ocaml/cic_unification/cicMkImplicit.ml
index 748307013f27168f25e7ba8ee4ea04064a5df3ef..b6aa1df419b5c60a9d5ace639bf865eea6ed35ab 100644 (file)
--- a/helm/ocaml/cic_unification/cicMkImplicit.ml
+++ b/helm/ocaml/cic_unification/cicMkImplicit.ml
@@ -51,6 +51,10 @@ let new_meta metasenv subst =
   in
   1 + aux (None, indexes)
 
+(* let apply_subst_context = CicMetaSubst.apply_subst_context;; *)
+(* questa o la precedente sembrano essere equivalenti come tempi *)
+let apply_subst_context _ context = context ;;
+
 let mk_implicit metasenv subst context =
   let newmeta = new_meta metasenv subst in
   let newuniv = CicUniv.fresh () in
@@ -58,7 +62,7 @@ let mk_implicit metasenv subst context =
     (* in the following mk_* functions we apply substitution to canonical
     * context since we have the invariant that the metasenv has already been
     * instantiated with subst *)
-  let context = CicMetaSubst.apply_subst_context subst context in
+  let context = apply_subst_context subst context in
   ([ newmeta, [], Cic.Sort (Cic.Type newuniv) ;
     (* TASSI: ?? *)
     newmeta + 1, context, Cic.Meta (newmeta, []);
@@ -68,7 +72,7 @@ let mk_implicit metasenv subst context =
 let mk_implicit_type metasenv subst context =
   let newmeta = new_meta metasenv subst in
   let newuniv = CicUniv.fresh () in
-  let context = CicMetaSubst.apply_subst_context subst context in
+  let context = apply_subst_context subst context in
   ([ newmeta, [], Cic.Sort (Cic.Type newuniv);
     (* TASSI: ?? *)
     newmeta + 1, context, Cic.Meta (newmeta, []) ] @metasenv,
@@ -84,7 +88,7 @@ let n_fresh_metas metasenv subst context n =
   if n = 0 then metasenv, []
   else 
     let irl = identity_relocation_list_for_metavariable context in
-    let context = CicMetaSubst.apply_subst_context subst context in
+    let context = apply_subst_context subst context in
     let newmeta = new_meta metasenv subst in
     let newuniv = CicUniv.fresh () in
     let rec aux newmeta n = 
@@ -100,7 +104,7 @@ let n_fresh_metas metasenv subst context n =
       
 let fresh_subst metasenv subst context uris = 
   let irl = identity_relocation_list_for_metavariable context in
-  let context = CicMetaSubst.apply_subst_context subst context in
+  let context = apply_subst_context subst context in
   let newmeta = new_meta metasenv subst in
   let newuniv = CicUniv.fresh () in
   let rec aux newmeta = function