X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FnCicParamod.ml;h=846a576c7861f9268aada91cc4642b98150d4e72;hb=08e552969f366bd18b5bb7515bbc514576a9b395;hp=a1e2a9ff5ea96b58cee526825ac456af267804f4;hpb=1341f9c234571b4172cd76cd84e7230039cb4642;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml
index a1e2a9ff5..846a576c7 100644
--- 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