From 2b1eb6d5cd2d3ff5024e48615df4b99692008690 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 28 Nov 2008 16:17:22 +0000
Subject: [PATCH] metas for terms have height 3

---
 .../components/ng_refiner/nCicMetaSubst.ml    | 32 +++++++++----------
 .../components/ng_refiner/nCicMetaSubst.mli   |  2 +-
 .../components/ng_refiner/nCicRefiner.ml      |  2 +-
 3 files changed, 17 insertions(+), 19 deletions(-)

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index 4c44221ad..5e72d90c7 100644
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -342,27 +342,25 @@ let delift metasenv subst context n l t =
 ;;
 
 let mk_meta ?name metasenv context ty = 
-  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
+  let tyof = function Some s -> Some ("typeof_"^s) | None -> None in
+  let rec mk_meta name n metasenv context = function
   | `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
+  | `Sort ->
+    let ty = NCic.Implicit (`Typeof n) in
+    mk_meta (tyof name) n metasenv [] (`WithType ty)
+  | `Type ->
+    let metasenv, ty, _ = 
+      mk_meta (tyof name) (newmeta ()) metasenv context `Sort in
+    mk_meta name n metasenv context (`WithType ty)
+  | `Term ->
+    let metasenv, ty, _ = 
+      mk_meta (tyof name) (newmeta ()) metasenv context `Type in
+    mk_meta name n metasenv context (`WithType ty)
+  in
+    mk_meta name (newmeta ()) metasenv context ty
 ;;
 
 let saturate ?(delta=0) metasenv context ty goal_arity =
diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli
index ca2bfb714..21ac5c3cc 100644
--- a/helm/software/components/ng_refiner/nCicMetaSubst.mli
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.mli
@@ -56,7 +56,7 @@ val restrict:
 val mk_meta: 
    ?name:string -> 
    NCic.metasenv -> NCic.context -> 
-    [ `WithType of NCic.term | `Term | `Type | `Typeless ] -> 
+    [ `WithType of NCic.term | `Term | `Type | `Sort ] -> 
     NCic.metasenv * NCic.term * NCic.term (* menv, instance, type *)
 
 (* returns the resulting type, the metasenv and the arguments *)
diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 05862d9da..8c6c94cb5 100644
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -40,7 +40,7 @@ let wrap_exc msg = function
 let exp_implicit metasenv context expty =
  let foo x = match expty with Some t -> `WithType t | None -> x in
  function      
-  | `Closed -> NCicMetaSubst.mk_meta metasenv [] (foo `Type)
+  | `Closed -> NCicMetaSubst.mk_meta metasenv [] (foo `Term)
   | `Type -> NCicMetaSubst.mk_meta metasenv context (foo `Type)
   | `Term -> NCicMetaSubst.mk_meta metasenv context (foo `Term)
   | _ -> assert false
-- 
2.39.2