new instantiate, only known bug is w.r.t. in/out scope and file matita/contribs/ng_as...

[helm.git] / helm / software / components / ng_paramodulation / nCicParamod.ml

diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml
index a1e2a9ff5ea96b58cee526825ac456af267804f4..846a576c7861f9268aada91cc4642b98150d4e72 100644 (file)
--- a/helm/software/components/ng_paramodulation/nCicParamod.ml
+++ b/helm/software/components/ng_paramodulation/nCicParamod.ml
@@ -51,7 +51,9 @@ let nparamod rdb metasenv subst context t table =
         let rec aux k metasenv = function
           | NCic.Meta _ as t -> metasenv, t
           | NCic.Implicit _ -> 
-              let metasenv,i,_,_=NCicMetaSubst.mk_meta metasenv context `Term in
+              let metasenv, i, _, _ =
+                NCicMetaSubst.mk_meta metasenv context `IsTerm 
+              in
               metasenv, NCic.Meta (i,(k,NCic.Irl (List.length context)))
           | t -> NCicUntrusted.map_term_fold_a 
                   (fun _ k -> k+1) k aux metasenv t