Merge PR coq#7013: Fixes coq#7011: Fix/CoFix were not considered in m…

…ain loop of tactic unification.

pretyping/unification.ml

@@ -837,6 +837,26 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
 	     with ex when precatchable_exception ex ->
 	       reduce curenvnb pb opt substn cM cN)
 
+        | Fix ((ln1,i1),(lna1,tl1,bl1)), Fix ((ln2,i2),(_,tl2,bl2)) when
+               Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 ->
+            (try
+             let opt' = {opt with at_top = true; with_types = false} in
+             let curenvnb' = Array.fold_right2 (fun na t -> push (na,t)) lna1 tl1 curenvnb in
+               Array.fold_left2 (unirec_rec curenvnb' CONV opt')
+               (Array.fold_left2 (unirec_rec curenvnb CONV opt') substn tl1 tl2) bl1 bl2
+             with ex when precatchable_exception ex ->
+               reduce curenvnb pb opt substn cM cN)
+
+        | CoFix (i1,(lna1,tl1,bl1)), CoFix (i2,(_,tl2,bl2)) when
+               Int.equal i1 i2 ->
+            (try
+             let opt' = {opt with at_top = true; with_types = false} in
+             let curenvnb' = Array.fold_right2 (fun na t -> push (na,t)) lna1 tl1 curenvnb in
+               Array.fold_left2 (unirec_rec curenvnb' CONV opt')
+               (Array.fold_left2 (unirec_rec curenvnb CONV opt') substn tl1 tl2) bl1 bl2
+             with ex when precatchable_exception ex ->
+               reduce curenvnb pb opt substn cM cN)
+
 	| App (f1,l1), _ when 
 	    (isMeta sigma f1 && use_metas_pattern_unification sigma flags nb l1
             || use_evars_pattern_unification flags && isAllowedEvar sigma flags f1) ->

test-suite/bugs/closed/7011.v

@@ -0,0 +1,16 @@
+(* Fix and Cofix were missing in tactic unification *)
+
+Goal exists e, (fix foo (n : nat) : nat := match n with O => e | S n' => foo n' end)
+               = (fix foo (n : nat) : nat := match n with O => O | S n' => foo n' end).
+Proof.
+  eexists.
+  reflexivity.
+Qed.
+
+CoInductive stream := cons : nat -> stream -> stream.
+
+Goal exists e, (cofix foo := cons e foo) = (cofix foo := cons 0 foo).
+Proof.
+  eexists.
+  reflexivity.
+Qed.