added sortification for (? args), untested code

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index e56832fd502656a764891b6ce4da49ebd065a3e5..d48dfaf460a4967a02aada9d8f7ee5f8bdecd03c 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -274,6 +274,14 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap =
            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, subst, lambda_Mj =
+             lambda_intros rdb metasenv subst context t args
+           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"))
@@ -289,15 +297,6 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap =
   in
   let tags, ctx, ty = NCicUtils.lookup_meta n metasenv in
   (* instantiation *)
-  
-  (* sortification:
-      - Meta sort === t -> check t is sort or sortify
-        - add tag `IsSort and set cc=[] to n and its pile
-        - se gli ancestor non sono sorte o meta... bum...
-          - cambiare in-place menv
-          - geneare meta fresh sorta e dall'alto al basso
-      - Meta _ === Meta sort -> sortify n (i.e. add `IsSort)
-       *)
   pp (lazy(string_of_int n ^ " := 111 = "^ 
     NCicPp.ppterm ~metasenv ~subst ~context t));
   let (metasenv, subst), t =