X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.mli;h=033ea1b1b4f53682a419a5856380f1a46ee912bd;hb=d072c3ea699cf33189d18d8431fda9750fc2eb93;hp=1d7b6729e11ee5d6be2db10be7f2bbe3c8e08ebd;hpb=002d456397be2f0046bb50356e80816f7296647d;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli
index 1d7b6729e..033ea1b1b 100644
--- a/helm/software/components/ng_refiner/nCicMetaSubst.mli
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.mli
@@ -57,7 +57,7 @@ val mk_meta:
    ?name:string -> 
    NCic.metasenv -> NCic.context -> 
     [ `WithType of NCic.term | `Term | `Type | `Sort ] -> 
-    NCic.metasenv * NCic.term * NCic.term (* menv, instance, type *)
+    NCic.metasenv * int * NCic.term * NCic.term (* menv,metano,instance,type *)
 
 (* returns the resulting type, the metasenv and the arguments *)
 val saturate: