Experimental support for Russell (coercions moving inside lambda & pattern

[helm.git] / helm / software / components / ng_refiner / nCicUnification.ml

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index c7b487461963a179bd6333232cefb7ce13385bbf..e521dd30144f7db95de3950996dd1c09cd8b54ac 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -50,7 +50,7 @@ let eta_reduce subst t =
           let _,_,t,_ = NCicUtils.lookup_subst i subst in
           let t = NCicSubstitution.subst_meta lc t in
           eat_lambdas ctx t
-        with Not_found -> ctx, t)
+        with NCicUtils.Subst_not_found _ -> ctx, t)
     | t -> ctx, t
   in
   let context_body = eat_lambdas [] t in
@@ -572,12 +572,8 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
              (NCicTypeChecker.typeof ~metasenv ~subst context meta)
           in
           let metasenv, subst = 
-           try
-            unify rdb test_eq_only metasenv subst context 
-              (C.Meta (i,l)) lambda_Mj swap
-           with UnificationFailure msg | Uncertain msg when not norm2->
-            (* failure: let's try again argument vs argument *)
-            raise (KeepReducing msg)
+           unify rdb test_eq_only metasenv subst context 
+            (C.Meta (i,l)) lambda_Mj swap
           in
           let metasenv, subst = 
             unify rdb test_eq_only metasenv subst context t1 t2 swap
@@ -612,14 +608,12 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
              with
                 Invalid_argument _ -> 
                  raise (Uncertain (mk_msg metasenv subst context t1 t2))
-              | UnificationFailure _ | Uncertain _ when not (norm1 && norm2) ->
-                 raise (KeepReducing (mk_msg metasenv subst context t1 t2))
               | KeepReducing _ | KeepReducingThis _ -> assert false
            in 
              metasenv, subst
 
        | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
-          C.Match (ref2,outtype2,term2,pl2)) ->
+          C.Match (ref2,outtype2,term2,pl2)) when Ref.eq ref1 ref2 ->
            let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
            let _,_,ty,_ = List.nth itl tyno in
            let rec remove_prods ~subst context ty = 
@@ -635,9 +629,9 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
              | C.Sort C.Prop -> true
              | _ -> false 
            in
-           if not (Ref.eq ref1 ref2) then 
+           (* if not (Ref.eq ref1 ref2) then 
              raise (Uncertain (mk_msg metasenv subst context t1 t2))
-           else
+           else*)
              let metasenv, subst = 
               unify rdb test_eq_only metasenv subst context outtype1 outtype2 swap in
              let metasenv, subst = 
@@ -660,6 +654,12 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
        | _ -> raise (KeepReducing (mk_msg metasenv subst context t1 t2))
      (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
     in
+    let fo_unif test_eq_only metasenv subst (norm1,t1 as nt1) (norm2,t2 as nt2)=
+     try fo_unif test_eq_only metasenv subst nt1 nt2
+     with
+      UnificationFailure _ | Uncertain _ when not norm1 || not norm2 ->
+       raise (KeepReducing (mk_msg metasenv subst context t1 t2))
+    in
     let try_hints metasenv subst (_,t1 as mt1) (_,t2 as mt2) (* exc*) =
     (*D*) inside 'H'; try let rc =  
      pp(lazy ("\nProblema:\n" ^