Merge PR #7013: Fixes #7011: Fix/CoFix were not considered in main loop of tactic unification.

2 files changed, 36 insertions, 0 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index b49291adb..5f7faa13e 100644
--- a/pretyping/unification.ml
+++ b/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) ->
diff --git a/test-suite/bugs/closed/7011.v b/test-suite/bugs/closed/7011.v
new file mode 100644
index 000000000..296e4e11e
--- /dev/null
+++ b/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.