X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=6f1d8718ae02d8c1b0998c1664c498b4959735f4;hb=HEAD;hp=6dfa7afee01c328cdbfa01d0e314fabee8d070f4;hpb=6120c5ba6c24eeeb2f932ba7e247a751c4216134;p=helm.git

diff --git a/matita/components/ng_refiner/nCicUnification.ml b/matita/components/ng_refiner/nCicUnification.ml
index 6dfa7afee..6f1d8718a 100644
--- a/matita/components/ng_refiner/nCicUnification.ml
+++ b/matita/components/ng_refiner/nCicUnification.ml
@@ -19,7 +19,7 @@ exception KeepReducingThis of
   string Lazy.t * (NCicReduction.machine * bool) * 
                   (NCicReduction.machine * bool) ;;
 
-let (===) x y = Pervasives.compare x y = 0 ;;
+let (===) x y = Stdlib.compare x y = 0 ;;
 
 let mk_msg (status:#NCic.status) metasenv subst context t1 t2 =
  (lazy (
@@ -140,7 +140,7 @@ let rec could_reduce status ~subst context =
   | C.Appl (C.Const (Ref.Ref (_,Ref.Fix (_,recno,_)))::args)
      when List.length args > recno ->
       let t = NCicReduction.whd status ~subst context (List.nth args recno) in
-        could_reduce status subst context t
+        could_reduce status ~subst context t
   | C.Match (_,_,he,_) ->
      let he = NCicReduction.whd status ~subst context he in
       could_reduce status ~subst context he
@@ -233,6 +233,31 @@ let rec sortfy status exc metasenv subst context t =
  in
   metasenv,subst,t
 
+let indfy status exc metasenv subst context t =
+ let t = NCicReduction.whd status ~subst context t in
+ let metasenv,subst =
+  match t with
+   | NCic.Const (Ref.Ref (_, Ref.Ind _))
+   | NCic.Appl (NCic.Const (Ref.Ref (_, Ref.Ind _))::_) -> metasenv, subst
+(*
+   | NCic.Meta (n,_) -> 
+      let attrs, context, ty = NCicUtils.lookup_meta n metasenv in
+      let kind = NCicUntrusted.kind_of_meta attrs in
+       if kind = `IsSort then
+        metasenv,subst
+       else
+        (match ty with
+          | NCic.Implicit (`Typeof _) ->
+              metasenv_to_subst n (`IsSort,[],ty) metasenv subst
+          | ty ->
+             let metasenv,subst,ty = sortfy status exc metasenv subst context ty in
+              metasenv_to_subst n (`IsSort,[],ty) metasenv subst)
+*)
+   | NCic.Implicit _ -> assert false
+   | _ -> raise exc
+ in
+  metasenv,subst,t
+
 let tipify status exc metasenv subst context t ty =
  let is_type attrs =
   match NCicUntrusted.kind_of_meta attrs with
@@ -251,7 +276,7 @@ let tipify status exc metasenv subst context t ty =
          let metasenv,subst,ty = sortfy status exc metasenv subst cc ty in
          let metasenv = 
            NCicUntrusted.replace_in_metasenv n
-            (fun attrs,cc,_ -> NCicUntrusted.set_kind `IsType attrs, cc, ty)
+            (fun (attrs,cc,_) -> NCicUntrusted.set_kind `IsType attrs, cc, ty)
             metasenv 
          in
           metasenv,subst,false
@@ -265,7 +290,7 @@ let tipify status exc metasenv subst context t ty =
           let metasenv,subst,ty = sortfy status exc metasenv subst cc ty in
           let subst = 
             NCicUntrusted.replace_in_subst n
-              (fun attrs,cc,bo,_->NCicUntrusted.set_kind `IsType attrs,cc,bo,ty)
+              (fun (attrs,cc,bo,_)->NCicUntrusted.set_kind `IsType attrs,cc,bo,ty)
              subst 
           in
            optimize_meta metasenv subst (NCicSubstitution.subst_meta status lc bo))
@@ -532,8 +557,7 @@ and fo_unif0 during_delift status swap test_eq_only metasenv subst context (norm
                i
           | NCic.Meta (i,_) -> (metasenv, subst), i
           | _ ->
-             raise (UnificationFailure (lazy "Locked term vs non
-              flexible term; probably not saturated enough yet!"))
+             raise (UnificationFailure (lazy "Locked term vs non flexible term; probably not saturated enough yet!"))
          in
           let t1 = NCicReduction.whd status ~subst context t1 in
           let j, lj =