sortification simplified

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 8e3cf216e962b549d0eb64ef730b23b60f9a4672..e56832fd502656a764891b6ce4da49ebd065a3e5 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -214,20 +214,14 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap =
        let t, ty_t = 
          try t, NCicTypeChecker.typeof ~subst ~metasenv context t 
          with 
-         | NCicTypeChecker.AssertFailure msg -> 
-              pp(lazy("we try to fix the sort\n"^Lazy.force msg^"\n"^NCicPp.ppmetasenv ~subst
-              metasenv));
+         | 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 begin
-                raise (UnificationFailure (lazy ("unable to fix sorts of: "^
-                  NCicPp.ppterm ~metasenv ~subst ~context t)))
-              end;
+              if ft == t then raise exn;
               (try ft, NCicTypeChecker.typeof ~subst ~metasenv context ft 
-               with NCicTypeChecker.AssertFailure _ -> 
-                 raise (UnificationFailure (lazy 
-                   ("fix sorts generated an ill-typed: "^
-                   NCicPp.ppterm ~metasenv ~subst ~context t))))
+               with NCicTypeChecker.AssertFailure _ -> raise exn)
          | NCicTypeChecker.TypeCheckerFailure msg ->
               prerr_endline (Lazy.force msg);
               prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
@@ -264,7 +258,7 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap =
     | _ -> false
   in
   let rec sortify metasenv subst = function
-    | NCic.Implicit (`Typeof _) 
+    | 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
@@ -273,15 +267,12 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap =
            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 [] (`WithType ty)
+             NCicMetaSubst.mk_meta metasenv ~attrs:[`IsSort] [] (`WithType ty)
            in
            pp(lazy("rimpiazzo " ^ string_of_int i^" con "^string_of_int j));
-           let metasenv,subst = unify test_eq_only metasenv subst context t m in
-           let j = if swap then i else j in
-           let tags, context, ty = NCicUtils.lookup_meta j metasenv in
-           let tags = `IsSort :: tags in
-           let metasenv = List.filter (fun x,_ -> x <> j) metasenv in
-           let metasenv = (j,(tags,context,ty)) ::metasenv in 
+           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 
     | t -> 
          if could_reduce t then raise (Uncertain(lazy "not a sort"))