more work

[helm.git] / helm / software / components / ng_refiner / nCicMetaSubst.ml

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index 967074a564fd0aaca79b44ea771cd2e0eae74fbf..72151deb802e4e1ca6f9c3c2f3349195a00a3090 100644 (file)
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -571,17 +571,35 @@ let delift_rels subst metasenv n t =
 *) 
 
 let mk_meta ?name metasenv context ty = 
-  let n = newmeta () in
-  let len = List.length context in
-  let menv_entry = (n, (name, context, ty)) in
-  menv_entry :: metasenv, NCic.Meta (n, (0,NCic.Irl len))
+  match ty with
+  | `Typeless ->
+    let n = newmeta () in
+    let ty = NCic.Implicit (`Typeof n) in
+    let menv_entry = (n, (name, context, ty)) in
+    menv_entry :: metasenv,NCic.Meta (n, (0,NCic.Irl (List.length context))), ty
+  | `Type 
+  | `Term ->
+    let context_for_ty = if ty = `Type then [] else context in
+    let n = newmeta () in
+    let ty_menv_entry = (n, (name,context_for_ty, NCic.Implicit (`Typeof n))) in
+    let m = newmeta () in
+    let ty = NCic.Meta (n, (0,NCic.Irl (List.length context_for_ty))) in
+    let menv_entry = (m, (name, context, ty)) in
+    menv_entry :: ty_menv_entry :: metasenv, 
+      NCic.Meta (m, (0,NCic.Irl (List.length context))), ty
+  | `WithType ty ->
+    let n = newmeta () in
+    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
 ;;
 
 let saturate ?(delta=0) metasenv context ty goal_arity =
  assert (goal_arity >= 0);
   let rec aux metasenv = function
    | NCic.Prod (name,s,t) ->
-       let metasenv1, arg = mk_meta ~name:name metasenv context s in            
+       let metasenv1, arg,_ = 
+          mk_meta ~name:name metasenv context (`WithType s) in            
        let t, metasenv1, args, pno = 
            aux metasenv1 (NCicSubstitution.subst arg t) 
        in