From f8d45b2e4fa7817d7ef8312b3bb8a7439bd7fb8c Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 22 Oct 2009 22:11:03 +0000
Subject: [PATCH] new instantiate, only known bug is w.r.t. in/out scope and
 file matita/contribs/ng_assembly/compiler/environment.ma

---
 .../grafite_engine/grafiteEngine.ml           |  11 +-
 helm/software/components/ng_kernel/nCic.ml    |   7 +-
 .../components/ng_kernel/nCicEnvironment.ml   |  50 ++-
 .../components/ng_kernel/nCicEnvironment.mli  |   6 +-
 helm/software/components/ng_kernel/nCicPp.ml  |   4 +-
 .../components/ng_kernel/nCicUntrusted.ml     |  31 ++
 .../components/ng_kernel/nCicUntrusted.mli    |   7 +
 .../ng_paramodulation/nCicParamod.ml          |   4 +-
 .../components/ng_refiner/nCicMetaSubst.ml    |  47 +-
 .../components/ng_refiner/nCicMetaSubst.mli   |   5 +-
 .../components/ng_refiner/nCicRefiner.ml      |  59 ++-
 .../components/ng_refiner/nCicUnifHint.ml     |   6 +-
 .../components/ng_refiner/nCicUnification.ml  | 414 +++++++++---------
 .../components/ng_refiner/nCicUnification.mli |   4 +-
 .../components/ng_tactics/nTacStatus.ml       |  19 +-
 .../components/ng_tactics/nTacStatus.mli      |   4 +-
 .../components/ng_tactics/nTactics.ml         |   9 +-
 .../ng_assembly/compiler/environment.ma       |   1 +
 .../matita/nlibrary/logic/destruct_bb.ma      |  15 +-
 19 files changed, 414 insertions(+), 289 deletions(-)

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index fa4b95253..fd8d776c1 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -868,11 +868,18 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
             List.fold_left
              (fun (status,uris) boxml ->
                try
-                let status,nuris =
+                let nstatus,nuris =
                  eval_ncommand opts status
                   ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml))
                 in
-                status, concat_nuris uris nuris
+                if nstatus#ng_mode <> `CommandMode then
+                  begin
+                    HLog.error "error in generating projection/eliminator";
+                    prerr_endline (NCicPp.ppobj nstatus#obj);
+                    nstatus, uris
+                  end
+                else
+                  nstatus, concat_nuris uris nuris
                with
                | MultiPassDisambiguator.DisambiguationError _ 
                | NCicTypeChecker.TypeCheckerFailure _ ->
diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml
index 32b79f02a..4490ee048 100644
--- a/helm/software/components/ng_kernel/nCic.ml
+++ b/helm/software/components/ng_kernel/nCic.ml
@@ -56,7 +56,12 @@ type hypothesis = string * context_entry   (* name, entry *)
 
 type context = hypothesis list
 
-type meta_attrs = [`Name of string | `IsSort | `InScope | `OutScope of int] list
+type meta_attr = 
+  [ `Name of string 
+  | `IsTerm | `IsType | `IsSort 
+  | `InScope | `OutScope of int]
+
+type meta_attrs = meta_attr list
 
 type conjecture =  meta_attrs * context * term
 
diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index df1fc849d..738329689 100644
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -27,8 +27,6 @@ let frozen_list = ref [];;
 let get_obj = ref (fun _ -> assert false);;
 let set_get_obj f = get_obj := f;;
 
-let type0 = []
-
 module F = Format 
 
 let rec ppsort f = function
@@ -154,7 +152,7 @@ let typeof_sort = function
   | C.Type t -> 
       raise (AssertFailure (lazy (
               "Cannot type an inferred type: "^ string_of_univ t)))
-  | C.Prop -> (C.Type type0)
+  | C.Prop -> (C.Type [])
 ;;
 
 let add_lt_constraint a b = 
@@ -172,8 +170,10 @@ let add_lt_constraint a b =
   | _ -> raise (BadConstraint
           (lazy "trying to add a constraint on an inferred universe"))
 ;;
+   
+let family_of = function (`CProp,_)::_ -> `CProp | _ -> `Type ;;
 
-let sup l =
+let sup fam l =
   match l with
   | [(`Type|`CProp),_] -> Some l
   | l ->
@@ -182,7 +182,6 @@ let sup l =
      (fun x -> lt_path_uri [] n1 x || (s1 <> `Succ && NUri.eq n1 x)) acc 
    in
    let solutions = List.fold_left bigger_than !universes l in
-   let fam = match l with (`CProp,_)::_ -> `CProp | _ -> `Type in
    let rec aux = function
      | [] -> None
      | u :: tl ->
@@ -192,6 +191,47 @@ let sup l =
     aux solutions
 ;;
 
+let sup l = sup (family_of l) l;;
+
+let inf ~strict fam l =
+  match l with
+  | [(`Type|`CProp),_] -> Some l
+  | [] -> None
+  | l ->
+   let smaller_than acc (_s1,n1) = 
+    List.filter
+     (fun x -> lt_path_uri [] x n1 || (not strict && NUri.eq n1 x)) acc 
+   in
+   let solutions = List.fold_left smaller_than !universes l in
+   let rec aux = function
+     | [] -> None
+     | u :: tl ->
+         if List.exists (lt_path_uri [] u) solutions then aux tl
+         else Some [fam,u]
+   in
+    aux solutions
+;;
+
+let inf ~strict l = inf ~strict (family_of l) l;;
+
+let rec universe_lt a b = 
+  match a, b with
+  | (((`Type|`Succ),_)::_ | []) , [`CProp,_] -> false
+  | l, ([((`Type|`CProp),b)] as orig_b) -> 
+       List.for_all 
+         (function 
+         | `Succ,_ as a -> 
+             (match sup [a] with
+             | None -> false
+             | Some x -> universe_lt x orig_b) 
+         | _, a -> lt_path a b) l
+  | _, ([] | [`Succ,_] | _::_::_) -> 
+     raise (BadConstraint (lazy (
+       "trying to check if "^string_of_univ a^
+       " is lt than the inferred universe " ^ string_of_univ b)))
+;;
+
+
 let allowed_sort_elimination s1 s2 =
   match s1, s2 with
   | C.Type (((`Type|`Succ),_)::_ | []), C.Type (((`Type|`Succ),_)::_ | []) 
diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli
index 35b97aa59..5128831be 100644
--- a/helm/software/components/ng_kernel/nCicEnvironment.mli
+++ b/helm/software/components/ng_kernel/nCicEnvironment.mli
@@ -53,9 +53,6 @@ val ppsort : Format.formatter -> NCic.sort -> unit
 val pp_constraints: unit -> string
 val get_universes: unit -> NCic.universe list
 
-(* The type of Prop, smaller than any other type *)
-val type0: NCic.universe
-
 (* use to type products *)
 val max: NCic.universe -> NCic.universe -> NCic.universe
 
@@ -65,6 +62,7 @@ exception BadConstraint of string Lazy.t;;
 val add_lt_constraint: NCic.universe -> NCic.universe -> unit
 val universe_eq: NCic.universe -> NCic.universe -> bool
 val universe_leq: NCic.universe -> NCic.universe -> bool
+val universe_lt: NCic.universe -> NCic.universe -> bool
 
 (* checks if s1 <= s2 *)
 val are_sorts_convertible: test_eq_only:bool -> NCic.sort -> NCic.sort -> bool
@@ -79,6 +77,8 @@ val typeof_sort: NCic.sort -> NCic.sort
 
 (* looks for a declared universe that is the least one above the input *)
 val sup : NCic.universe -> NCic.universe option
+val inf : strict:bool -> NCic.universe -> NCic.universe option
+val family_of : NCic.universe -> [ `CProp | `Type ]
 
 (* =========== /universes ============= *)
 
diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index 1058a48cc..6131a7daf 100644
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -224,7 +224,9 @@ let ppmetaattrs =
     String.concat ","
      (List.map
        (function
-           `IsSort -> "sort"
+         | `IsTerm -> "term"
+         | `IsType -> "type"
+         | `IsSort -> "sort"
          | `Name n -> "name=" ^ n
          | `InScope -> "in_scope"
          | `OutScope n -> "out_scope:" ^ string_of_int n
diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml
index b48db58ec..771f3070b 100644
--- a/helm/software/components/ng_kernel/nCicUntrusted.ml
+++ b/helm/software/components/ng_kernel/nCicUntrusted.ml
@@ -244,3 +244,34 @@ let rec apply_subst_metasenv subst = function
 (* hide optional arg *)
 let apply_subst s c t = apply_subst s c t;;
 
+
+type meta_kind = [ `IsSort | `IsType | `IsTerm ]
+
+let is_kind x = x = `IsSort || x = `IsType || x = `IsTerm ;;
+
+let kind_of_meta l =
+  try 
+    (match List.find is_kind l with
+    | `IsSort | `IsType | `IsTerm as x -> x
+    | _ -> assert false)
+  with 
+   Not_found -> assert false
+;;
+
+let rec replace_in_metasenv i f = function
+  | [] -> assert false
+  | (j,e)::tl when j=i -> (i,f e) :: tl
+  | x::tl -> x :: replace_in_metasenv i f tl
+;;
+          
+let set_kind newkind attrs = 
+  newkind :: List.filter (fun x -> not (is_kind x)) attrs 
+;;
+
+let max_kind k1 k2 = 
+  match k1, k2 with
+  | `IsSort, _ | _, `IsSort -> `IsSort
+  | `IsType, _ | _, `IsType -> `IsType
+  | _ -> `IsTerm
+;;
+
diff --git a/helm/software/components/ng_kernel/nCicUntrusted.mli b/helm/software/components/ng_kernel/nCicUntrusted.mli
index 1df92163d..9f5ab0fd5 100644
--- a/helm/software/components/ng_kernel/nCicUntrusted.mli
+++ b/helm/software/components/ng_kernel/nCicUntrusted.mli
@@ -20,6 +20,13 @@ val map_obj_kind:
 
 val metas_of_term : NCic.substitution -> NCic.context -> NCic.term -> int list
 
+type meta_kind = [ `IsSort | `IsType | `IsTerm ]
+val kind_of_meta: NCic.meta_attrs -> meta_kind
+val set_kind: meta_kind -> NCic.meta_attrs -> NCic.meta_attrs 
+val replace_in_metasenv: 
+  int -> (NCic.conjecture -> NCic.conjecture) -> NCic.metasenv -> NCic.metasenv
+val max_kind: meta_kind -> meta_kind -> meta_kind
+
 module NCicHash : Hashtbl.S with type key = NCic.term
 
 val mk_appl : NCic.term -> NCic.term list -> NCic.term 
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
diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index 421194abd..81b577093 100644
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -461,26 +461,31 @@ let delift ~unify metasenv subst context n l t =
         raise (MetaSubstFailure msg)
 ;;
 
-let mk_meta ?(attrs=[]) metasenv context ty = 
-  let tyof = List.map (function `Name s -> `Name ("typeof_"^s) | x -> x) in
-  let rec mk_meta attrs n metasenv context = function
-  | `WithType ty ->
-    let len = List.length context in
-    let menv_entry = (n, (attrs, context, ty)) in
-    menv_entry :: metasenv, n, NCic.Meta (n, (0,NCic.Irl len)), ty
-  | `Sort ->
-    let ty = NCic.Implicit (`Typeof n) in
-    mk_meta (`IsSort::tyof attrs) n metasenv [] (`WithType ty)
-  | `Type ->
-    let metasenv, _, ty, _ = 
-      mk_meta (tyof attrs) (newmeta ()) metasenv context `Sort in
-    mk_meta attrs n metasenv context (`WithType ty)
-  | `Term ->
-    let metasenv, _, ty, _ = 
-      mk_meta (tyof attrs) (newmeta ()) metasenv context `Type in
-    mk_meta attrs n metasenv context (`WithType ty)
-  in
-    mk_meta attrs (newmeta ()) metasenv context ty
+let mk_meta ?(attrs=[]) metasenv context ?with_type kind = 
+  assert(kind <> `IsSort || context = []);
+  let n = newmeta () in
+  let ty= match with_type with None-> NCic.Implicit (`Typeof n)| Some x ->x in
+  let len = List.length context in
+  let attrs = (kind :> NCic.meta_attr) :: attrs in
+  let menv_entry = (n, (attrs, context, ty)) in
+  menv_entry :: metasenv, n, NCic.Meta (n, (0,NCic.Irl len)), ty
+;;
+
+let extend_meta metasenv n =
+ try
+  let attrs,cc,ty = NCicUtils.lookup_meta n metasenv in 
+  (match ty with 
+  | NCic.Implicit (`Typeof _) -> 
+      let mk_meta context kind =
+        let metasenv, _, ty, _ = mk_meta metasenv context kind in
+        (n, (attrs, cc, ty)) :: List.filter (fun x,_ -> x <> n) metasenv, ty
+      in
+      (match NCicUntrusted.kind_of_meta attrs with
+       | `IsSort 
+       | `IsType -> mk_meta [] `IsSort
+       | `IsTerm -> mk_meta cc `IsType)
+  | ty -> metasenv, ty)
+ with NCicUtils.Meta_not_found _ -> assert false
 ;;
 
 let saturate ?(delta=0) metasenv subst context ty goal_arity =
@@ -488,7 +493,7 @@ let saturate ?(delta=0) metasenv subst context ty goal_arity =
   let rec aux metasenv = function
    | NCic.Prod (name,s,t) as ty ->
        let metasenv1, _, arg,_ = 
-          mk_meta ~attrs:[`Name name] metasenv context (`WithType s) in
+          mk_meta ~attrs:[`Name name] metasenv context ~with_type:s `IsTerm in
        let t, metasenv1, args, pno = 
            aux metasenv1 (NCicSubstitution.subst arg t) 
        in
diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli
index 4cce96095..0cedc5258 100644
--- a/helm/software/components/ng_refiner/nCicMetaSubst.mli
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.mli
@@ -48,9 +48,12 @@ val restrict:
 val mk_meta: 
    ?attrs:NCic.meta_attrs -> 
    NCic.metasenv -> NCic.context -> 
-    [ `WithType of NCic.term | `Term | `Type | `Sort ] -> 
+    ?with_type:NCic.term -> NCicUntrusted.meta_kind ->
     NCic.metasenv * int * NCic.term * NCic.term (* menv,metano,instance,type *)
 
+(* extend_meta m n: n must be in m *)
+val extend_meta: NCic.metasenv -> int -> NCic.metasenv * NCic.term
+
 (* returns the resulting type, the metasenv and the arguments *)
 val saturate:
     ?delta:int -> NCic.metasenv -> NCic.substitution -> 
diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index c3765f3f0..8c92d3328 100644
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -57,12 +57,11 @@ let wrap_exc msg = function
   | e -> raise e
 ;;
 
-let exp_implicit rdb ~localise metasenv subst context expty t =
- let foo x = function Some t -> `WithType t | None -> x in
+let exp_implicit rdb ~localise metasenv subst context with_type t =
  function      
   | `Closed ->
       let metasenv,subst,expty =
-       match expty with
+       match with_type with
           None -> metasenv,subst,None
         | Some typ ->
            let (metasenv,subst),typ =
@@ -80,11 +79,12 @@ let exp_implicit rdb ~localise metasenv subst context expty t =
            in
             metasenv,subst,Some typ
       in
-       NCicMetaSubst.mk_meta metasenv [] (foo `Term expty),subst
-  | `Type -> NCicMetaSubst.mk_meta metasenv context (foo `Type expty),subst
-  | `Term -> NCicMetaSubst.mk_meta metasenv context (foo `Term expty),subst
+       NCicMetaSubst.mk_meta metasenv [] ?with_type:expty `IsTerm,subst
+  | `Type -> NCicMetaSubst.mk_meta metasenv context ?with_type `IsType,subst
+  | `Term -> NCicMetaSubst.mk_meta metasenv context ?with_type `IsTerm,subst
   | `Tagged s ->
-      NCicMetaSubst.mk_meta ~attrs:[`Name s] metasenv context (foo `Term expty),subst
+      NCicMetaSubst.mk_meta 
+        ~attrs:[`Name s] metasenv context ?with_type `IsTerm,subst
   | `Vector ->
       raise (RefineFailure (lazy (localise t, "A vector of implicit terms " ^
        "can only be used in argument position")))
@@ -106,7 +106,7 @@ let check_allowed_sort_elimination rdb localise r orig =
      match arity1 with
      | C.Prod (name,so1,de1) (* , t ==?== C.Prod _ *) ->
         let metasenv, _, meta, _ = 
-          NCicMetaSubst.mk_meta metasenv ((name,C.Decl so1)::context) `Type 
+          NCicMetaSubst.mk_meta metasenv ((name,C.Decl so1)::context) `IsType 
         in
         let metasenv, subst = 
           try NCicUnification.unify rdb metasenv subst context 
@@ -119,7 +119,7 @@ let check_allowed_sort_elimination rdb localise r orig =
         aux metasenv subst ((name, C.Decl so1)::context)
          (mkapp (NCicSubstitution.lift 1 ind) (C.Rel 1)) de1 meta
      | C.Sort _ (* , t ==?== C.Prod _ *) ->
-        let metasenv, _, meta, _ = NCicMetaSubst.mk_meta metasenv [] `Type in
+        let metasenv, _, meta, _ = NCicMetaSubst.mk_meta metasenv [] `IsSort in
         let metasenv, subst = 
           try NCicUnification.unify rdb metasenv subst context 
                 arity2 (C.Prod ("_", ind, meta)) 
@@ -198,21 +198,16 @@ let rec typeof rdb
          let (metasenv,_,t,ty),subst =
            exp_implicit rdb ~localise metasenv subst context expty t infos
          in
+         if expty = None then
+          typeof_aux metasenv subst context None t
+         else
           metasenv, subst, t, ty 
     | C.Meta (n,l) as t -> 
-       let ty =
+       let metasenv, ty =
         try
-         let _,_,_,ty = NCicUtils.lookup_subst n subst in ty 
-        with NCicUtils.Subst_not_found _ -> try
-         let _,_,ty = NCicUtils.lookup_meta n metasenv in 
-         match ty with C.Implicit _ -> 
-                 prerr_endline (string_of_int n);
-                 prerr_endline (NCicPp.ppmetasenv ~subst metasenv);
-                 prerr_endline (NCicPp.ppsubst ~metasenv subst);
-                 assert false | _ -> ty 
-        with NCicUtils.Meta_not_found _ ->
-         raise (AssertFailure (lazy (Printf.sprintf
-          "%s not found" (NCicPp.ppterm ~subst ~metasenv ~context t))))
+         let _,_,_,ty = NCicUtils.lookup_subst n subst in metasenv, ty 
+        with NCicUtils.Subst_not_found _ ->
+         NCicMetaSubst.extend_meta metasenv n
        in
        metasenv, subst, t, NCicSubstitution.subst_meta l ty
     | C.Const _ -> 
@@ -252,7 +247,7 @@ let rec typeof rdb
              (try 
                pp(lazy("Force source to: "^NCicPp.ppterm ~metasenv ~subst
                   ~context exp_s));
-               NCicUnification.unify rdb metasenv subst context s exp_s,exp_ty_t
+               NCicUnification.unify ~test_eq_only:true rdb metasenv subst context s exp_s,exp_ty_t
              with exc -> raise (wrap_exc (lazy (localise orig_s, Printf.sprintf
                "Source type %s was expected to be %s" (NCicPp.ppterm ~metasenv
                ~subst ~context s) (NCicPp.ppterm ~metasenv ~subst ~context
@@ -343,16 +338,11 @@ let rec typeof rdb
       (* next lines are to do a subst-expansion of the outtype, so
          that when it becomes a beta-abstraction, the beta-redex is
          fired during substitution *)
-      (*CSC: this is instantiate! should we move it from tactics to the
-             refiner? I think so! *)
-      let metasenv,metanoouttype,newouttype,metaoutsort =
-       NCicMetaSubst.mk_meta metasenv context `Term in
-      let metasenv,subst =
-       NCicUnification.unify rdb metasenv subst context outsort metaoutsort in
-      let metasenv =
-       List.filter (function (j,_) -> j <> metanoouttype) metasenv in
+      let _,fresh_metanoouttype,newouttype,_ =
+       NCicMetaSubst.mk_meta metasenv context `IsTerm in
       let subst =
-       (metanoouttype,([`Name "outtype"],context,outtype,metaoutsort))::subst in
+       (fresh_metanoouttype,([`Name "outtype"],context,outtype,outsort))
+         ::subst in
       let outtype = newouttype in
 
       (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
@@ -476,7 +466,10 @@ and force_to_sort rdb metasenv subst context t orig_t localise ty =
   | C.Sort _ as ty -> metasenv, subst, t, ty 
   | ty -> 
       try_coercions rdb ~localise metasenv subst context
-        t orig_t ty (NCic.Sort (NCic.Type NCicEnvironment.type0)) false 
+        t orig_t ty (NCic.Sort (NCic.Type 
+          (match NCicEnvironment.get_universes () with
+           | x::_ -> x 
+           | _ -> assert false))) false 
          (Uncertain (lazy (localise orig_t, 
          "The type of " ^ NCicPp.ppterm ~metasenv ~subst ~context t
          ^ " is not a sort: " ^ NCicPp.ppterm ~metasenv ~subst ~context ty)))
@@ -565,7 +558,7 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he
           let name = guess_name subst context ty_arg in
           let metasenv, _, meta, _ = 
             NCicMetaSubst.mk_meta metasenv 
-              ((name,C.Decl ty_arg) :: context) `Type
+              ((name,C.Decl ty_arg) :: context) `IsType
           in
           let flex_prod = C.Prod (name, ty_arg, meta) in
           (* next line grants that ty_args is a type *)
diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml
index 313fbbd0d..0f0708d63 100644
--- a/helm/software/components/ng_refiner/nCicUnifHint.ml
+++ b/helm/software/components/ng_refiner/nCicUnifHint.ml
@@ -212,7 +212,8 @@ let saturate ?(delta=0) metasenv subst context ty goal_arity =
    | NCic.Prod (name,s,t) as ty ->
        let metasenv1, _, arg,_ = 
           NCicMetaSubst.mk_meta ~attrs:[`Name name] metasenv context
-           (`WithType s) in
+           ~with_type:s `IsTerm 
+       in
        let t, metasenv1, args, pno = 
            aux metasenv1 (NCicSubstitution.subst arg t) 
        in
@@ -284,7 +285,8 @@ let look_for_hint hdb metasenv subst context t1 t2 =
            | NCic.LetIn (name,ty,bo,t) ->
                let m,_,i,_=
                  NCicMetaSubst.mk_meta ~attrs:[`Name name] m context
-                  (`WithType ty)in
+                  ~with_type:ty `IsTerm 
+               in
                let t = NCicSubstitution.subst i t in
                aux () (m, (i,bo)::l) t
            | t -> NCicUntrusted.map_term_fold_a (fun _ () -> ()) () aux acc t
diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 8e84c015d..edf116d17 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -115,26 +115,8 @@ let ppmetasenv ~subst m = "\nmenv:\n" ^ NCicPp.ppmetasenv ~subst m;;
 
 let ppcontext ~metasenv:_metasenv ~subst:_subst _context = "";;
 let ppmetasenv ~subst:_subst _metasenv = "";;
-
-let fix_sorts swap exc t =
-  let rec aux () = function
-    | NCic.Sort (NCic.Type u) as orig ->
-        if swap then
-         match NCicEnvironment.sup u with
-         | None ->
-            prerr_endline ("no sup for " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] orig) ;
-            raise exc
-         | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1)
-        else
-         NCic.Sort (NCic.Type (
-           match NCicEnvironment.sup NCicEnvironment.type0 with 
-           | Some x -> x
-           | _ -> assert false))
-    | NCic.Meta _ as orig -> orig
-    | t -> NCicUtils.map (fun _ _ -> ()) () aux t
-  in
-    aux () t
-;;
+let ppterm ~metasenv ~subst ~context = NCicPp.ppterm ~metasenv ~subst ~context;;
+(* let ppterm ~metasenv:_ ~subst:_ ~context:_ _ = "";; *)
 
 let is_locked n subst =
    try
@@ -162,11 +144,11 @@ let rec could_reduce =
 ;;
 
 let rec lambda_intros rdb metasenv subst context argsno ty =
- pp (lazy ("LAMBDA INTROS: " ^ NCicPp.ppterm ~metasenv ~subst ~context ty));
+ pp (lazy ("LAMBDA INTROS: " ^ ppterm ~metasenv ~subst ~context ty));
  match argsno with
     0 -> 
        let metasenv, _, bo, _ = 
-         NCicMetaSubst.mk_meta metasenv context (`WithType ty)
+         NCicMetaSubst.mk_meta metasenv context ~with_type:ty `IsTerm
        in
        metasenv, bo
   | _ ->
@@ -179,181 +161,221 @@ let rec lambda_intros rdb metasenv subst context argsno ty =
            metasenv,C.Lambda (n,so,bo)
        | _ -> assert false)
 ;;
+  
+let unopt exc = function None -> raise exc | Some x -> x ;;
+
+let fix metasenv subst is_sup test_eq_only exc t =
+  let rec aux test_eq_only metasenv = function
+    | NCic.Prod (n,so,ta) ->
+       let metasenv,so = aux true metasenv so in
+       let metasenv,ta = aux test_eq_only metasenv ta in
+        metasenv,NCic.Prod (n,so,ta)
+    | NCic.Sort (NCic.Type [(`CProp|`Type),_]) as orig when test_eq_only ->
+       metasenv,orig
+    | NCic.Sort (NCic.Type _) when test_eq_only -> raise exc
+    | NCic.Sort (NCic.Type u) when is_sup ->
+       metasenv, NCic.Sort (NCic.Type (unopt exc (NCicEnvironment.sup u)))
+    | NCic.Sort (NCic.Type u) ->
+       metasenv, NCic.Sort (NCic.Type 
+         (unopt exc (NCicEnvironment.inf ~strict:false u)))
+    | NCic.Meta (n,_) as orig ->
+        (try 
+          let _,_,_,_ = NCicUtils.lookup_subst n subst in metasenv,orig
+         with NCicUtils.Subst_not_found _ -> 
+          let metasenv, _ = NCicMetaSubst.extend_meta metasenv n in
+           metasenv, orig)
+    | t ->
+      NCicUntrusted.map_term_fold_a (fun _ x -> x) test_eq_only aux metasenv t
+  in
+   aux test_eq_only metasenv t
+;;
+
+let rec sortfy exc metasenv subst = function
+  | NCic.Sort _ as orig -> metasenv, orig
+  | NCic.Meta (n,lc) -> 
+      let attrs, context, ty = NCicUtils.lookup_meta n metasenv in
+      let kind = NCicUntrusted.kind_of_meta attrs in
+      kindfy exc metasenv subst context n lc ty kind `IsSort
+  | NCic.Implicit _ -> assert false
+  | _ -> raise exc
+
+and kindfy exc metasenv subst context n lc ty kind kind2 = 
+  match kind, ty, kind2 with
+  | `IsSort, _, _ -> assert(snd lc = NCic.Irl 0); metasenv, NCic.Meta(n,lc)
+  | k1, NCic.Implicit (`Typeof _), (`IsType|`IsTerm as k2) -> 
+     let k = NCicUntrusted.max_kind k1 k2 in
+     let metasenv = 
+       NCicUntrusted.replace_in_metasenv n
+         (fun attrs,cc,ty -> NCicUntrusted.set_kind k attrs, cc, ty) metasenv 
+     in
+     metasenv, NCic.Meta(n,lc)
+  | _, NCic.Implicit (`Typeof _), `IsSort ->
+     let metasenv = 
+       NCicUntrusted.replace_in_metasenv n
+        (fun attrs,_,ty-> NCicUntrusted.set_kind `IsSort attrs,[],ty) metasenv 
+     in
+     metasenv, NCic.Meta (n,(0,NCic.Irl 0))
+  | _, ty, `IsSort ->
+     let metasenv, ty = 
+       sortfy exc metasenv subst (NCicReduction.whd ~subst context ty) 
+     in
+     let metasenv = 
+       NCicUntrusted.replace_in_metasenv n
+        (fun attrs,_,_-> NCicUntrusted.set_kind `IsSort attrs,[],ty) metasenv 
+     in
+     metasenv, NCic.Meta (n,(0,NCic.Irl 0))
+  | k1, _, k2 when NCicUntrusted.max_kind k1 k2 = k1-> metasenv, NCic.Meta(n,lc)
+  | `IsTerm, ty, `IsType ->
+     let metasenv, ty = 
+       sortfy exc metasenv subst (NCicReduction.whd ~subst context ty) 
+     in
+     let metasenv = 
+       NCicUntrusted.replace_in_metasenv n
+        (fun attrs,cc,_-> NCicUntrusted.set_kind `IsType attrs,cc,ty) metasenv 
+     in
+     metasenv, NCic.Meta (n,lc)
+  | _ -> assert false (* XXX *)
 
-let rec instantiate rdb test_eq_only metasenv subst context n lc t swap =
+and instantiate rdb test_eq_only metasenv subst context n lc t swap =
  (*D*)  inside 'I'; try let rc =  
-         pp (lazy(string_of_int n ^ " :=?= "^
-           NCicPp.ppterm ~metasenv ~subst ~context t));
-  let unify test_eq_only m s c t1 t2 = 
-    if swap then unify rdb test_eq_only m s c t2 t1 
-    else unify rdb test_eq_only m s c t1 t2
-  in
-  let has_tag = List.exists in
-  let tags, _, ty = NCicUtils.lookup_meta n metasenv in
-  (* on the types *)
-  let metasenv, subst, t = 
-    match ty with 
-    | NCic.Implicit (`Typeof _) -> 
-         pp(lazy("meta with no type"));
-         assert(has_tag ((=)`IsSort) tags); 
-         metasenv, subst, t
-    | _ ->
-       let exc_to_be =
-        UnificationFailure (mk_msg metasenv subst context (NCic.Meta (n,lc)) t)
-       in
-       let t, ty_t = 
-         try t, NCicTypeChecker.typeof ~subst ~metasenv context t 
-         with 
-         | NCicTypeChecker.AssertFailure msg as exn -> 
-              pp(lazy("we try to fix the sort\n"^
-                Lazy.force msg^"\n"^NCicPp.ppmetasenv ~subst metasenv));
-              let ft = fix_sorts swap exc_to_be t in
-              pp(lazy("unable to fix the sort"));
-              if ft == t then raise exn;
-              (try ft, NCicTypeChecker.typeof ~subst ~metasenv context ft 
-               with NCicTypeChecker.AssertFailure _ -> raise exn)
-         | NCicTypeChecker.TypeCheckerFailure msg ->
-              prerr_endline (Lazy.force msg);
-              prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
-              prerr_endline (ppcontext ~metasenv ~subst context); 
-              prerr_endline (ppmetasenv ~subst metasenv);
-              assert false
-       in
-       match ty_t with
-       | NCic.Implicit (`Typeof _) -> 
-           raise (UnificationFailure(lazy "trying to unify a term with a type"))
-       | _ -> 
-          let lty = NCicSubstitution.subst_meta lc ty in
-          pp (lazy ("On the types: " ^
-              NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === " ^ 
-              NCicPp.ppterm ~metasenv ~subst ~context ty_t)); 
-          let metasenv,subst = 
-           try unify test_eq_only metasenv subst context lty ty_t
-           with NCicEnvironment.BadConstraint _ as exc ->
-            let ty_t = fix_sorts swap exc_to_be ty_t in 
-             try unify test_eq_only metasenv subst context lty ty_t
-             with 
-             | NCicEnvironment.BadConstraint _ 
-             | UnificationFailure _ -> raise exc 
-          in
-           metasenv, subst, t
-  in 
-  (* viral sortification *)
-  let is_sort metasenv subst context t = 
-    match NCicReduction.whd ~subst context t with
-    | NCic.Meta (i,_) ->
-         let tags, _, _ = NCicUtils.lookup_meta i metasenv in
-         has_tag ((=) `IsSort) tags
-    | NCic.Sort _ -> true
-    | _ -> false
+  pp (lazy(string_of_int n^" :=?= "^ppterm ~metasenv ~subst ~context t));
+  let exc = 
+    UnificationFailure (mk_msg metasenv subst context (NCic.Meta (n,lc)) t) in
+  let move_to_subst i attrs cc t ty metasenv subst =
+    let metasenv = List.remove_assoc i metasenv in
+    pp (lazy(string_of_int n ^ " :==> "^ 
+      ppterm ~metasenv ~subst ~context:cc t));
+    metasenv, (i,(attrs, cc, t, ty)) :: subst
   in
-  let rec sortify metasenv subst = function
-    | NCic.Implicit (`Typeof _) -> assert false 
-    | NCic.Sort _ as t -> metasenv, subst, t, 0
-    | NCic.Meta (i,_) as t -> 
-         let tags, context, ty = NCicUtils.lookup_meta i metasenv in
-         if has_tag ((=) `IsSort) tags then metasenv, subst, t, i
-         else
-           let ty = NCicReduction.whd ~subst context ty in
-           let metasenv, subst, ty, _ = sortify metasenv subst ty in
-           let metasenv, j, m, _ = 
-             NCicMetaSubst.mk_meta metasenv ~attrs:[`IsSort] [] (`WithType ty)
+  let delift_to_subst test_eq_only n lc attrs cc t ty context metasenv subst =
+    pp (lazy(string_of_int n ^ " := 111 = "^ 
+      ppterm ~metasenv ~subst ~context t));
+    let (metasenv, subst), t = 
+      try 
+        NCicMetaSubst.delift 
+         ~unify:(fun m s c t1 t2 -> 
+           let ind = !indent in
+           let res = 
+                   try Some (unify rdb test_eq_only m s c t1 t2 )
+             with UnificationFailure _ | Uncertain _ -> None
            in
-           pp(lazy("rimpiazzo " ^ string_of_int i^" con "^string_of_int j));
-           let subst_entry = i, (tags, context, m, ty) in
-           let subst = subst_entry :: subst in
-           let metasenv = List.filter (fun x,_ -> i <> x) metasenv in
-           metasenv, subst, m, j 
-    | NCic.Appl (NCic.Meta _ as hd :: args) as t -> 
-           let metasenv, lambda_Mj =
-             lambda_intros rdb metasenv subst context (List.length args)
-              (NCicTypeChecker.typeof ~metasenv ~subst context hd)
-           in
-           let metasenv,subst= unify true metasenv subst context hd lambda_Mj in
-           let t = NCicReduction.whd ~subst context t in
-           let _result = sortify metasenv subst t in       
-           (* untested, maybe dead, code *) assert false;
-    | t -> 
-         if could_reduce t then raise (Uncertain(lazy "not a sort"))
-         else raise (UnificationFailure(lazy "not a sort"))
-  in
-  let metasenv, subst, _, n = 
-    if has_tag ((=) `IsSort) tags then
-      let m,s,x,_ = sortify metasenv subst (NCicReduction.whd ~subst context t)
-      in m,s,x,n
-    else if is_sort metasenv subst context t then
-      sortify metasenv subst (NCic.Meta (n,lc))
-    else
-      metasenv, subst, NCic.Rel ~-1,n
-  in
-  let tags, ctx, ty = NCicUtils.lookup_meta n metasenv in
-  (* instantiation *)
-  pp (lazy(string_of_int n ^ " := 111 = "^ 
-    NCicPp.ppterm ~metasenv ~subst ~context t));
-  let (metasenv, subst), t = 
-    try 
-      NCicMetaSubst.delift 
-       ~unify:(fun m s c t1 t2 -> 
-         let ind = !indent in
-         let res = 
-           try Some (unify test_eq_only m s c t1 t2 )
-           with UnificationFailure _ | Uncertain _ -> None
-         in
-         indent := ind; res) 
-       metasenv subst context n lc t
-    with NCicMetaSubst.Uncertain msg -> 
-         pp (lazy ("delift fails: " ^ Lazy.force msg));
-         raise (Uncertain msg)
-    | NCicMetaSubst.MetaSubstFailure msg -> 
-         pp (lazy ("delift fails: " ^ Lazy.force msg));
-         raise (UnificationFailure msg)
-  in
-         pp (lazy(string_of_int n ^ " := 222 = "^
-           NCicPp.ppterm ~metasenv ~subst ~context:ctx t
-         ^ ppmetasenv ~subst metasenv));
-  (* Unifying the types may have already instantiated n. *)
-  try
-    let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
-    let oldt = NCicSubstitution.subst_meta lc oldt in
-    let t = NCicSubstitution.subst_meta lc t in
-    (* conjecture: always fail --> occur check *)
-    unify test_eq_only metasenv subst context oldt t
-  with NCicUtils.Subst_not_found _ -> 
-    let metasenv, tags = 
-      let rec aux = function
-        | NCic.Meta (j,lc) -> 
-            (try 
-              let _, _, t, _ = NCicUtils.lookup_subst j subst in
-              aux (NCicSubstitution.subst_meta lc t)
-            with NCicUtils.Subst_not_found _ -> 
-              let tags', ctx, ty = NCicUtils.lookup_meta j metasenv in
-              let metasenv = List.remove_assoc j metasenv in
-              let tags = tags @ tags' in
-              (j, (tags, ctx, ty)) :: metasenv, tags)
-        | _ -> metasenv, tags
-      in 
-        aux t
+           indent := ind; res) 
+         metasenv subst context n lc t
+      with NCicMetaSubst.Uncertain msg -> 
+           pp (lazy ("delift is uncertain: " ^ Lazy.force msg));
+           raise (Uncertain msg)
+      | NCicMetaSubst.MetaSubstFailure msg -> 
+           pp (lazy ("delift fails: " ^ Lazy.force msg));
+           raise (UnificationFailure msg)
     in
-    (* by cumulativity when unify(?,Type_i) 
-     * we could ? := Type_j with j <= i... *)
-    let subst = (n, (tags, ctx, t, ty)) :: subst in
-    pp (lazy ("?"^string_of_int n^" := "^NCicPp.ppterm
-      ~metasenv ~subst ~context (NCicSubstitution.subst_meta lc t)));
-    let metasenv = 
-      List.filter (fun (m,_) -> not (n = m)) metasenv 
-    in
-    metasenv, subst
+    pp (lazy(string_of_int n ^ " := 222 = "^
+      ppterm ~metasenv ~subst ~context:cc t^ppmetasenv ~subst metasenv));
+    (* Unifying the types may have already instantiated n. *)
+    try
+      let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
+      let oldt = NCicSubstitution.subst_meta lc oldt in
+      let t = NCicSubstitution.subst_meta lc t in
+      (* conjecture: always fail --> occur check *)
+      unify rdb test_eq_only metasenv subst context t oldt
+    with NCicUtils.Subst_not_found _ -> 
+      move_to_subst n attrs cc t ty metasenv subst
+  in
+  let attrs, cc, ty = NCicUtils.lookup_meta n metasenv in
+  match NCicUntrusted.kind_of_meta attrs, ty, t, swap with
+  | `IsSort, (NCic.Implicit (`Typeof _) as bot), NCic.Sort (NCic.Type u),false->
+      pp(lazy("1"));
+      let u = NCicEnvironment.inf ~strict:false u in
+      let t = NCic.Sort (NCic.Type (unopt exc u)) in
+      move_to_subst n attrs cc t bot metasenv subst  
+  | `IsSort, (NCic.Implicit (`Typeof _) as bot), NCic.Sort (NCic.Type u),true ->
+      pp(lazy("2"));
+      let u = NCicEnvironment.sup u in
+      let t = NCic.Sort (NCic.Type (unopt exc u)) in
+      move_to_subst n attrs cc t bot metasenv subst  
+  | `IsSort, (NCic.Sort(NCic.Type u1) as ty), NCic.Sort (NCic.Type u2), false ->
+      pp(lazy("3"));
+      let u = 
+        NCicEnvironment.inf ~strict:false (u1 @
+          unopt exc (NCicEnvironment.inf ~strict:true u2)) 
+      in
+      let t = NCic.Sort (NCic.Type (unopt exc u)) in
+      move_to_subst n attrs cc t ty metasenv subst  
+  | `IsSort, (NCic.Sort(NCic.Type u1) as ty), NCic.Sort (NCic.Type u2), true ->
+      pp(lazy("4"));
+      let u = unopt exc (NCicEnvironment.sup u2) in
+      if NCicEnvironment.universe_lt u u1 then
+        let t = NCic.Sort (NCic.Type u) in
+        move_to_subst n attrs cc t ty metasenv subst  
+      else (raise exc)
+  | _, _, NCic.Meta(m,lcm), _ when List.mem_assoc m subst ->
+      (* deref needed for locked metas, maybe should be done outside *)
+      let _,_,bo,_ = NCicUtils.lookup_subst m subst in
+      let bo = NCicSubstitution.subst_meta lcm bo in
+      instantiate rdb test_eq_only metasenv subst context n lc bo swap
+  | kind, (NCic.Implicit (`Typeof _) as bot),  NCic.Meta(m,lcm), _ ->
+      pp(lazy("5"));
+      let attrsm, ccm, tym = NCicUtils.lookup_meta m metasenv in
+      let kindm = NCicUntrusted.kind_of_meta attrsm in
+      let metasenv, t = kindfy exc metasenv subst ccm m lcm tym kindm kind in
+      move_to_subst n attrs cc t bot metasenv subst  
+  | kind, ty,  (NCic.Meta(m,_) as t), _ when 
+    let _, _, tym = NCicUtils.lookup_meta m metasenv in
+    (match tym with NCic.Implicit (`Typeof _) -> true | _ -> false) ->
+      pp(lazy("6"));
+      let attrsm, _, _ = NCicUtils.lookup_meta m metasenv in
+      let kindm = NCicUntrusted.kind_of_meta attrsm in
+      let metasenv, _ = kindfy exc metasenv subst cc n lc ty kind kindm in
+      let attrs, cc, ty = NCicUtils.lookup_meta n metasenv in
+      let metasenv = NCicUntrusted.replace_in_metasenv m
+        (fun _,_,_ -> attrs,cc,ty) metasenv
+      in
+      (* XXX *)move_to_subst n attrs cc t ty metasenv subst  
+  | kind, ty,  NCic.Meta(m,lcm), _ ->
+      pp(lazy("7"));
+      let ty_t, ccm, kindm = 
+        let at, ccm, tym = NCicUtils.lookup_meta m metasenv in
+        NCicSubstitution.subst_meta lcm tym, ccm, NCicUntrusted.kind_of_meta at
+      in
+      let lty = NCicSubstitution.subst_meta lc ty in
+      pp (lazy ("On the types: " ^
+        ppterm ~metasenv ~subst ~context lty ^
+        (if test_eq_only then " === " else "=<=") ^
+        ppterm ~metasenv ~subst ~context ty_t)); 
+      let metasenv, subst = 
+        unify rdb test_eq_only metasenv subst context ty_t lty
+      in
+      let metasenv, t = kindfy exc metasenv subst ccm m lcm ty_t kindm kind in
+      delift_to_subst test_eq_only n lc attrs cc t ty context metasenv subst 
+  | _, (NCic.Implicit (`Typeof _) as bot), t, swap ->
+      pp(lazy("8"));
+      let metasenv, t = fix metasenv subst swap test_eq_only exc t in
+(*       let ty_t = NCicTypeChecker.typeof ~metasenv ~subst context t in *)
+      (* ty andrebbe deliftato *)
+      delift_to_subst test_eq_only n lc attrs cc t bot context metasenv subst 
+  | _, ty, t, swap ->
+      pp(lazy("9"));
+      let lty = NCicSubstitution.subst_meta lc ty in
+      let metasenv, t = fix metasenv subst swap test_eq_only exc t in
+      let ty_t = NCicTypeChecker.typeof ~metasenv ~subst context t in
+      pp (lazy ("On the types: " ^
+        ppterm ~metasenv ~subst ~context lty ^
+        (if test_eq_only then " === " else "=<=") ^
+        ppterm ~metasenv ~subst ~context ty_t)); 
+      let metasenv, subst = 
+        unify rdb test_eq_only metasenv subst context ty_t lty
+      in
+      delift_to_subst test_eq_only n lc attrs cc t ty context metasenv subst 
  (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
 
 and unify rdb test_eq_only metasenv subst context t1 t2 =
  (*D*) inside 'U'; try let rc =
    let fo_unif test_eq_only metasenv subst (norm1,t1) (norm2,t2) =
     (*D*) inside 'F'; try let rc =  
-     pp (lazy("  " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^ 
-         NCicPp.ppterm ~metasenv ~subst ~context t2 ^ ppmetasenv
+     pp (lazy("  " ^ ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^ 
+         ppterm ~metasenv ~subst ~context t2 ^ ppmetasenv
          ~subst metasenv));
-     pp (lazy("  " ^ NCicPp.ppterm ~metasenv ~subst:[] ~context t1 ^ " ==??== " ^ 
-         NCicPp.ppterm ~metasenv ~subst:[] ~context t2 ^ ppmetasenv
+     pp (lazy("  " ^ ppterm ~metasenv ~subst:[] ~context t1 ^ " ==??== " ^ 
+         ppterm ~metasenv ~subst:[] ~context t2 ^ ppmetasenv
          ~subst metasenv));
      if t1 === t2 then
        metasenv, subst
@@ -614,8 +636,8 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
     let try_hints metasenv subst (_,t1 as mt1) (_,t2 as mt2) (* exc*) =
     (*D*) inside 'H'; try let rc =  
      pp(lazy ("\nProblema:\n" ^
-        NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " =?= " ^
-        NCicPp.ppterm ~metasenv ~subst ~context t2));
+        ppterm ~metasenv ~subst ~context t1 ^ " =?= " ^
+        ppterm ~metasenv ~subst ~context t2));
       let candidates = 
         NCicUnifHint.look_for_hint rdb metasenv subst context t1 t2
       in
@@ -626,11 +648,11 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
               String.concat "\n"
                 (List.map 
                   (fun (a,b) ->
-                   NCicPp.ppterm ~metasenv ~subst ~context a ^  " =?= " ^
-                   NCicPp.ppterm ~metasenv ~subst ~context b) premises) ^
+                   ppterm ~metasenv ~subst ~context a ^  " =?= " ^
+                   ppterm ~metasenv ~subst ~context b) premises) ^
               "\n-------------------------------------------\n"^
-              NCicPp.ppterm ~metasenv ~subst ~context c1 ^  " = " ^
-              NCicPp.ppterm ~metasenv ~subst ~context c2));
+              ppterm ~metasenv ~subst ~context c1 ^  " = " ^
+              ppterm ~metasenv ~subst ~context c2));
             try 
     (*D*) inside 'K'; try let rc =  
               let metasenv,subst = 
@@ -657,7 +679,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
       NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
       NCicReduction.reduce_machine ~delta:max_int ~subst context m2
     in
-    let fo_unif_w_hints test_eq_only metasenv subst (xx1,t1 as m1) (xx2,t2 as m2) =
+    let fo_unif_w_hints test_eq_only metasenv subst (_,t1 as m1) (_,t2 as m2) =
       try fo_unif test_eq_only metasenv subst m1 m2
       with 
       | UnificationFailure _ as exn -> raise exn
@@ -703,10 +725,10 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
       | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
      (*D*) inside 'M'; try let rc = 
          pp (lazy("UM: " ^
-           NCicPp.ppterm ~metasenv ~subst ~context 
+           ppterm ~metasenv ~subst ~context 
              (NCicReduction.unwind (k1,e1,t1,s1)) ^
            " === " ^ 
-           NCicPp.ppterm ~metasenv ~subst ~context 
+           ppterm ~metasenv ~subst ~context 
              (NCicReduction.unwind (k2,e2,t2,s2))));
          pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
           let relevance = [] (* TO BE UNDERSTOOD 
@@ -789,4 +811,6 @@ let unify rdb ?(test_eq_only=false) =
   indent := "";      
   unify rdb test_eq_only;;
 
-let fix_sorts = fix_sorts true (UnificationFailure (lazy "no sup"));;
+let fix_sorts m s =
+  fix m s true false (UnificationFailure (lazy "no sup"))
+;;
diff --git a/helm/software/components/ng_refiner/nCicUnification.mli b/helm/software/components/ng_refiner/nCicUnification.mli
index 83a59b64c..fef24b2d5 100644
--- a/helm/software/components/ng_refiner/nCicUnification.mli
+++ b/helm/software/components/ng_refiner/nCicUnification.mli
@@ -23,7 +23,9 @@ val unify :
    NCic.metasenv * NCic.substitution
 
 (* this should be moved elsewhere *)
-val fix_sorts: NCic.term -> NCic.term
+val fix_sorts: 
+  NCic.metasenv -> NCic.substitution -> 
+    NCic.term -> NCic.metasenv * NCic.term
 
 (* delift_type_wrt_terms st m s c t args
  *   lift t (length args) 
diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index ed583fdaf..0bef3a794 100644
--- a/helm/software/components/ng_tactics/nTacStatus.ml
+++ b/helm/software/components/ng_tactics/nTacStatus.ml
@@ -194,10 +194,13 @@ let unify status ctx a b =
 ;;
 let unify a b c d = wrap "unify" (unify a b c) d;;
 
-let fix_sorts (ctx,t) =
+let fix_sorts status (ctx,t) =
  let f () =
-  let t = NCicUnification.fix_sorts t in
-   ctx,t
+  let name,height,metasenv,subst,obj = status#obj in
+  let metasenv, t = 
+    NCicUnification.fix_sorts metasenv subst t in
+  let status = status#set_obj (name,height,metasenv,subst,obj) in
+   status, (ctx,t)
  in
   wrap "fix_sorts" f ()
 ;;
@@ -248,13 +251,13 @@ let instantiate_with_ast status i t =
   to_subst status i (gname,context,t,gty)
 ;;
 
-let mk_meta status ?(attrs=[]) ctx bo_or_ty =
+let mk_meta status ?(attrs=[]) ctx bo_or_ty kind =
   match bo_or_ty with
   | `Decl ty ->
       let status, (_,ty) = relocate status ctx ty in
       let n,h,metasenv,subst,o = status#obj in
       let metasenv, _, instance, _ = 
-        NCicMetaSubst.mk_meta ~attrs metasenv ctx (`WithType ty)
+        NCicMetaSubst.mk_meta ~attrs metasenv ctx ~with_type:ty kind
       in
       let status = status#set_obj (n,h,metasenv,subst,o) in
       status, (ctx,instance)
@@ -263,7 +266,7 @@ let mk_meta status ?(attrs=[]) ctx bo_or_ty =
       let status, (_,ty) = typeof status ctx bo in
       let n,h,metasenv,subst,o = status#obj in
       let metasenv, metano, instance, _ = 
-        NCicMetaSubst.mk_meta ~attrs metasenv ctx (`WithType ty) in
+        NCicMetaSubst.mk_meta ~attrs metasenv ctx ~with_type:ty kind in
       let metasenv = List.filter (fun j,_ -> j <> metano) metasenv in
       let subst = (metano, (attrs, ctx, bo_, ty)) :: subst in
       let status = status#set_obj (n,h,metasenv,subst,o) in
@@ -271,11 +274,11 @@ let mk_meta status ?(attrs=[]) ctx bo_or_ty =
 ;;
 
 let mk_in_scope status t =
-  mk_meta status ~attrs:[`InScope] (ctx_of t) (`Def t)
+  mk_meta status ~attrs:[`InScope] (ctx_of t) (`Def t) `IsTerm
 ;;
 
 let mk_out_scope n status t = 
-  mk_meta status ~attrs:[`OutScope n] (ctx_of t) (`Def t)
+  mk_meta status ~attrs:[`OutScope n] (ctx_of t) (`Def t) `IsTerm
 ;;
 
 (* the following unification problem will be driven by 
diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli
index f3bdd5aa1..ec9f7738a 100644
--- a/helm/software/components/ng_tactics/nTacStatus.mli
+++ b/helm/software/components/ng_tactics/nTacStatus.mli
@@ -56,7 +56,7 @@ val refine:
   'status * cic_term * cic_term (* status, term, type *)
 val apply_subst:
  #pstatus as 'status -> NCic.context -> cic_term -> 'status * cic_term
-val fix_sorts: cic_term -> cic_term
+val fix_sorts: #pstatus as 'status -> cic_term -> 'status * cic_term
 val saturate :
  #pstatus as 'status -> ?delta:int -> cic_term -> 'status * cic_term * cic_term list
 val metas_of_term : #pstatus as 'status -> cic_term -> int list
@@ -64,7 +64,7 @@ val metas_of_term : #pstatus as 'status -> cic_term -> int list
 val get_goalty: #pstatus -> int -> cic_term
 val mk_meta: 
  #pstatus as 'status -> ?attrs:NCic.meta_attrs -> NCic.context ->
-   [ `Decl of cic_term | `Def of cic_term ] ->
+   [ `Decl of cic_term | `Def of cic_term ] -> NCicUntrusted.meta_kind ->
      'status * cic_term
 val instantiate: #pstatus as 'status -> int -> cic_term -> 'status
 val instantiate_with_ast: #pstatus as 'status -> int -> tactic_term -> 'status
diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 9834cce8a..a4a72a180 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -368,7 +368,7 @@ let select0_tac ~where:(wanted,hyps,where) ~job  =
    let newgoalty = mk_cic_term newgoalctx newgoalty in
 
    let status, instance = 
-     mk_meta status newgoalctx (`Decl newgoalty) 
+     mk_meta status newgoalctx (`Decl newgoalty) `IsTerm
    in
    instantiate status goal instance)
 ;;
@@ -395,7 +395,6 @@ let generalize_tac ~where =
  let l = ref [] in
  block_tac [ 
    select_tac ~where ~job:(`Collect l) true; 
-   print_tac true "ha selezionato?";
    (fun s -> distribute_tac (fun status goal ->
       let goalty = get_goalty status goal in
       let status,canon,rest =
@@ -423,8 +422,8 @@ let cut_tac t =
  block_tac [ 
   exact_tac ("",0, Ast.Appl [Ast.Implicit `JustOne; Ast.Implicit `JustOne]);
   branch_tac;
-   pos_tac [2]; exact_tac t;
-   shift_tac; pos_tac [1]; skip_tac;
+   pos_tac [3]; exact_tac t;
+   shift_tac; pos_tac [2]; skip_tac;
   merge_tac ]
 ;;
 
@@ -497,7 +496,7 @@ let analyze_indty_tac ~what indtyref =
 let sort_of_goal_tac sortref = distribute_tac (fun status goal ->
   let goalty = get_goalty status goal in
   let status,sort = typeof status (ctx_of goalty) goalty in
-  let sort = fix_sorts sort in
+  let status, sort = fix_sorts status sort in
   let status, sort = term_of_cic_term status sort (ctx_of goalty) in
    sortref := sort;
    status)
diff --git a/helm/software/matita/contribs/ng_assembly/compiler/environment.ma b/helm/software/matita/contribs/ng_assembly/compiler/environment.ma
index d62b6fec3..4467f332c 100755
--- a/helm/software/matita/contribs/ng_assembly/compiler/environment.ma
+++ b/helm/software/matita/contribs/ng_assembly/compiler/environment.ma
@@ -46,6 +46,7 @@ ndefinition defined_envList ≝
 nlemma defined_envList_S : ∀d.∀l:env_list (S d).defined_envList (S d) l.
  #d; #l;
  ngeneralize in match (refl_eq ? (S d));
+ XXX nuova instantiate!
  (* S d = S d → ? e' in realta' eq nat (S d) (S d) ... *)
  ncases l in ⊢ (? ? % ? → %);
  ##[ ##1: #dsc; #H; nelim (nat_destruct_0_S … H)
diff --git a/helm/software/matita/nlibrary/logic/destruct_bb.ma b/helm/software/matita/nlibrary/logic/destruct_bb.ma
index f167be393..f188bf80f 100644
--- a/helm/software/matita/nlibrary/logic/destruct_bb.ma
+++ b/helm/software/matita/nlibrary/logic/destruct_bb.ma
@@ -41,17 +41,16 @@ definition r1 : ∀T0,T1,a0,b0,e0.T1 a0 → T1 b0 ≝
 include "logic/equality.ma".
   
 ndefinition R1 ≝ eq_rect_Type0.
-
 ndefinition R2 :
   ∀T0:Type[0].
   ∀a0:T0.
   ∀T1:∀x0:T0. a0=x0 → Type[0].
   ∀a1:T1 a0 (refl ? a0).
-  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ??? a1 ? p0 = x1 → Type[0].
+  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ? a0 ? a1 ? p0 = x1 → Type[0].
   ∀b0:T0.
   ∀e0:a0 = b0.
   ∀b1: T1 b0 e0.
-  ∀e1:R1 ??? a1 ? e0 = b1.
+  ∀e1:R1 ? a0 ? a1 ? e0 = b1. (* eccezine se tolgo a0 *)
   ∀so:T2 a0 (refl ? a0) a1 (refl ? a1).T2 b0 e0 b1 e1.
 #T0;#a0;#T1;#a1;#T2;#b0;#e0;#b1;#e1;#H;
 napply (eq_rect_Type0 ????? e1);
@@ -64,16 +63,16 @@ ndefinition R3 :
   ∀a0:T0.
   ∀T1:∀x0:T0. a0=x0 → Type[0].
   ∀a1:T1 a0 (refl ? a0).
-  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ??? a1 ? p0 = x1 → Type[0].
+  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ? a0 ? a1 ? p0 = x1 → Type[0].
   ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
-  ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ??? a1 ? p0 = x1.
-      ∀x2:T2 x0 p0 x1 p1.R2 ???? ? ? p0 ? p1 a2 = x2 → Type[0].
+  ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ? a0 ? a1 ? p0 = x1.
+      ∀x2:T2 x0 p0 x1 p1.R2 ? a0 ? a1 ? ? p0 ? p1 a2 = x2 → Type[0].
   ∀b0:T0.
   ∀e0:a0 = b0.
   ∀b1: T1 b0 e0.
-  ∀e1:R1 ??? a1 ? e0 = b1.
+  ∀e1:R1 ? a0 ? a1 ? e0 = b1.
   ∀b2: T2 b0 e0 b1 e1.
-  ∀e2:R2 ???? ? ? e0 ? e1 a2 = b2.
+  ∀e2:R2 ? a0 ? a1 ? ? e0 ? e1 a2 = b2.
   ∀so:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).T3 b0 e0 b1 e1 b2 e2.
 #T0;#a0;#T1;#a1;#T2;#a2;#T3;#b0;#e0;#b1;#e1;#b2;#e2;#H;
 napply (eq_rect_Type0 ????? e2);
-- 
2.39.2