X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.ml;h=3f2f43df09d30d1449ec0ea2828be8b1276c0c0b;hb=e898ca2563cc4dfbd328efc7aa3a4ff86feaec92;hp=dd3485df093fb799b70dfb1175fdad50ff6d832a;hpb=246f3c2f2d26655129efacf830ecff47094795b4;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index dd3485df0..3f2f43df0 100644
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -347,16 +347,16 @@ let mk_meta ?name metasenv context ty =
   | `WithType ty ->
     let len = List.length context in
     let menv_entry = (n, (name, context, ty)) in
-    menv_entry :: metasenv, NCic.Meta (n, (0,NCic.Irl len)), ty
+    menv_entry :: metasenv, n, NCic.Meta (n, (0,NCic.Irl len)), ty
   | `Sort ->
     let ty = NCic.Implicit (`Typeof n) in
     mk_meta (tyof name) n metasenv [] (`WithType ty)
   | `Type ->
-    let metasenv, ty, _ = 
+    let metasenv, _, ty, _ = 
       mk_meta (tyof name) (newmeta ()) metasenv context `Sort in
     mk_meta name n metasenv context (`WithType ty)
   | `Term ->
-    let metasenv, ty, _ = 
+    let metasenv, _, ty, _ = 
       mk_meta (tyof name) (newmeta ()) metasenv context `Type in
     mk_meta name n metasenv context (`WithType ty)
   in
@@ -367,7 +367,7 @@ let saturate ?(delta=0) metasenv subst context ty goal_arity =
  assert (goal_arity >= 0);
   let rec aux metasenv = function
    | NCic.Prod (name,s,t) as ty ->
-       let metasenv1, arg,_ = 
+       let metasenv1, _, arg,_ = 
           mk_meta ~name:name metasenv context (`WithType s) in            
        let t, metasenv1, args, pno = 
            aux metasenv1 (NCicSubstitution.subst arg t)