Many fixes in unification:

- Restore failure when types don't unify in [unify_types] (undoing
r12075) but try to be more clever about cumulativity using the meta's
[instance_status] information.
- Fix second-order abstraction when K is not allowed to ensure that
we don't unify twice with the same subterm in
[w_unify_to_subterm_list]. A more elaborate solution would be give the
list to [w_unify_to_subterm] so that it keeps going when it finds an
already-found instantiation.
- Two "obvious" errors fixed: taking the wrong instance status when
unifying with a meta on the right and forgoting type equations in
[w_merge].


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12136 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 24 insertions, 16 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 64d96adc9..83c7b8370 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -206,7 +206,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 	| _, Meta k when not (dependent cN cM) -> 
 	    (* Here we check that [cM] does not contain any local variables *)
 	    if nb = 0 then
-              (sigma,(k,cM,snd (extract_instance_status pb))::metasubst,evarsubst)
+              (sigma,(k,cM,fst (extract_instance_status pb))::metasubst,evarsubst)
 	    else if noccur_between 1 nb cM
 	    then
               (sigma,(k,lift (-nb) cM,fst (extract_instance_status pb))::metasubst,
@@ -545,19 +545,25 @@ let w_coerce env evd mv c =
   let mvty = Typing.meta_type evd mv in
   w_coerce_to_type env evd c cty mvty
 
-let unify_to_type env sigma flags c u =
+let unify_to_type env sigma flags c status u =
   let c = refresh_universes c in
   let t = get_type_of env sigma c in
   let t = Tacred.hnf_constr env sigma (nf_betaiota sigma (nf_meta sigma t)) in
   let u = Tacred.hnf_constr env sigma u in
-  try unify_0 env sigma Cumul flags t u
-  with e when precatchable_exception e -> (sigma,[],[])
+    if status = IsSuperType then
+      unify_0 env sigma Cumul flags u t
+    else if status = IsSubType then
+      unify_0 env sigma Cumul flags t u
+    else 
+      try unify_0 env sigma Cumul flags t u
+      with e when precatchable_exception e ->
+	unify_0 env sigma Cumul flags u t
 
-let unify_type env sigma flags mv c =
+let unify_type env sigma flags mv status c =
   let mvty = Typing.meta_type sigma mv in
-  if occur_meta_or_existential mvty or is_arity env sigma mvty then
-    unify_to_type env sigma flags c mvty
-  else (sigma,[],[])
+(*   if occur_meta_or_existential mvty or is_arity env sigma mvty then *)
+    unify_to_type env sigma flags c status mvty
+(*   else (sigma,[],[]) *)
 
 (* Move metas that may need coercion at the end of the list of instances *)
 
@@ -614,10 +620,10 @@ let w_merge env with_types flags (evd,metas,evars) =
 	  if with_types & to_type <> TypeProcessed then
 	    if to_type = CoerceToType then
               (* Some coercion may have to be inserted *)
-	      (w_coerce env evd mv c,([],[])),[]
+	      (w_coerce env evd mv c,([],[])),eqns
 	    else
               (* No coercion needed: delay the unification of types *)
-	      ((evd,c),([],[])),(mv,c)::eqns
+	      ((evd,c),([],[])),(mv,status,c)::eqns
 	  else 
 	    ((evd,c),([],[])),eqns in
 	  if meta_defined evd mv then
@@ -637,8 +643,8 @@ let w_merge env with_types flags (evd,metas,evars) =
 
     (* Process type eqns *)
     match eqns with
-    | (mv,c)::eqns ->
-        let (evd,metas,evars) = unify_type env evd flags mv c in 
+    | (mv,status,c)::eqns ->
+        let (evd,metas,evars) = unify_type env evd flags mv status c in 
         w_merge_rec evd metas evars eqns
     | [] -> evd
 		
@@ -721,7 +727,7 @@ let w_unify_to_subterm env ?(flags=default_unify_flags) (op,cl) evd =
     let cl = strip_outer_cast cl in
     (try 
        if closed0 cl 
-       then w_unify_0 env topconv flags op cl evd,cl
+       then w_typed_unify env topconv flags op cl evd,cl
        else error "Bound 1"
      with ex when precatchable_exception ex ->
        (match kind_of_term cl with 
@@ -784,9 +790,12 @@ let w_unify_to_subterm_list env flags allow_K oplist t evd =
           try 
 	    (* This is up to delta for subterms w/o metas ... *)
 	    w_unify_to_subterm env ~flags (strip_outer_cast op,t) evd
-          with PretypeError (env,NoOccurrenceFound _) when allow_K -> (evd,op)
+	  with PretypeError (env,NoOccurrenceFound _) when allow_K -> (evd,op)
         in 
-	(evd',cl::l)
+	  if not allow_K && (* ensure we found a different instance *)
+	    List.exists (fun op -> eq_constr op cl) l
+	  then error "Unify_to_subterm_list"
+	  else (evd',cl::l)
       else if allow_K or dependent op t then
 	(evd,op::l)
       else
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index d5cb2882c..773807120 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -340,7 +340,6 @@ rewrite N.spec_of_N, Z_of_N_abs, Zabs_eq; auto.
 fold (recursion a f n).
 apply recursion_wd; auto.
 red; auto.
-red; auto.
 unfold N.to_N.
 
 rewrite N.spec_succ.