X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=7d8a45d0e6d9b660ca9f618e7dc25e7b3e858a24;hb=48c011f52853dd106dbf9cbbd1b9da61277fba3b;hp=b4bc32fe6035dc7bded70504a0826222ca2d63dc;hpb=bf4eb0f3a5b5ff262ad32271a8ba6f171e68c1f0;p=helm.git

diff --git a/matita/components/ng_refiner/nCicUnification.ml b/matita/components/ng_refiner/nCicUnification.ml
index b4bc32fe6..7d8a45d0e 100644
--- a/matita/components/ng_refiner/nCicUnification.ml
+++ b/matita/components/ng_refiner/nCicUnification.ml
@@ -140,8 +140,10 @@ 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
-  | C.Match (_,_,arg,_) -> could_reduce status ~subst context arg
+        could_reduce status ~subst context t
+  | C.Match (_,_,he,_) ->
+     let he = NCicReduction.whd status ~subst context he in
+      could_reduce status ~subst context he
   | C.Appl (he::_) -> could_reduce status ~subst context he
   | C.Sort _ | C.Rel _ | C.Prod _ | C.Lambda _ | C.Const _ -> false
   | C.Appl [] | C.LetIn _ | C.Implicit _ -> assert false
@@ -231,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
@@ -412,6 +439,8 @@ and unify_for_delift status metasenv subst context t1 t2 =
    try Some
     (fo_unif_w_hints true status false true(*test_eq_only*) metasenv subst
       context (false,t1) (false,t2))
+    (*(unify status true(*test_eq_only*) metasenv subst
+      context t1 t2 false)*)
    with UnificationFailure _ | Uncertain _ | KeepReducingThis _ -> None
  in
  indent := ind; res