Back-porting from new Matita:

- GREAT: when unifying ?1 : Type[i]  with ?2: Type[j] the unifier
  randomly tried to instantiate ?1 with ?2 even when j > i, yielding to
  an unification error later on. In turn, this created that horrible
  behaviour of rewriting that failed if you did not pass enough types
  to the lemma.
- in rewriting the argument is now automatically saturated

These two fixes together allow most of the time to write simply >f as we
did in the old system.

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index e2f6a7090ded821e685a5bb6ce3c8be1ed3293e2..fcc76b0adc5bf72b38129bd36a3ddca7952d4676 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -382,8 +382,8 @@ let rec instantiate rdb test_eq_only metasenv subst context n lc t swap =
        | _ ->
         let lty = NCicSubstitution.subst_meta lc ty in
         pp (lazy ("On the types: " ^
-          ppterm ~metasenv ~subst ~context lty ^ "=<=" ^
-          ppterm ~metasenv ~subst ~context ty_t)); 
+          ppterm ~metasenv ~subst ~context ty_t ^ "=<=" ^
+          ppterm ~metasenv ~subst ~context lty)); 
         let metasenv, subst = 
           unify rdb false metasenv subst context ty_t lty false
         in
@@ -559,6 +559,17 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
               len2 < len1 && cc2 = fst (HExtlib.split_nth len2 cc1) ->
           instantiate rdb test_eq_only metasenv subst context m lc'
             (NCicReduction.head_beta_reduce ~subst t1) (not swap)
+       | C.Meta (n,lc), C.Meta (m,lc') when
+          let _,_,tyn = NCicUtils.lookup_meta n metasenv in
+          let _,_,tym = NCicUtils.lookup_meta m metasenv in
+          let tyn = NCicSubstitution.subst_meta lc tyn in
+          let tym = NCicSubstitution.subst_meta lc tym in
+           match tyn,tym with
+              NCic.Sort NCic.Type u1, NCic.Sort NCic.Type u2 ->
+               NCicEnvironment.universe_lt u1 u2
+            | _,_ -> false ->
+          instantiate rdb test_eq_only metasenv subst context m lc'
+            (NCicReduction.head_beta_reduce ~subst t1) (not swap)
        | C.Meta (n,lc), t -> 
           instantiate rdb test_eq_only metasenv subst context n lc 
             (NCicReduction.head_beta_reduce ~subst t) swap
@@ -865,7 +876,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
          | KeepReducing _ -> assert false
          | KeepReducingThis _ ->
             assert (not (norm1 && norm2));
-           unif_machines metasenv subst (small_delta_step ~subst m1 m2)
+            unif_machines metasenv subst (small_delta_step ~subst m1 m2)
          | UnificationFailure _ | Uncertain _ when (not (norm1 && norm2))
            -> unif_machines metasenv subst (small_delta_step ~subst m1 m2)
          | UnificationFailure msg