Backport PR coq#11241: Unfortunate Coq 8.10 bug with "cofix with" tac…

…tic syntax
ppedrot · Dec 7, 2019 · 58b346a · 58b346a
2 parents 61a2ada + 7eeb0d2
commit 58b346a
Show file tree

Hide file tree

Showing 4 changed files with 15 additions and 5 deletions.
diff --git a/doc/changelog/05-tactic-language/11241-master+bug-cofix-with-8.10.rst b/doc/changelog/05-tactic-language/11241-master+bug-cofix-with-8.10.rst
@@ -0,0 +1,4 @@
+- **Fixed:**
+  Syntax of tactic `cofix ... with ...` was broken from Coq 8.10.
+  (`#11241 <https://github.com/coq/coq/pull/11241>`_,
+  by Hugo Herbelin).
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
@@ -135,7 +135,7 @@ let mk_cofix_tac (loc,id,bl,ann,ty) =
       ~hdr:"Constr:mk_cofix_tac"
       (Pp.str"Annotation forbidden in cofix expression.")) ann in
   let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,bk,t)) bl in
-  (id,CAst.make ~loc @@ CProdN(bl,ty))
+  (id,if bl = [] then ty else CAst.make ~loc @@ CProdN(bl,ty))
 
 (* Functions overloaded by quotifier *)
 let destruction_arg_of_constr (c,lbind as clbind) = match lbind with

diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
@@ -1210,7 +1210,3 @@ Proof.
  constructor.
  trivial.
 Qed.
-
-
-
-
diff --git a/test-suite/success/cofixtac.v b/test-suite/success/cofixtac.v
@@ -0,0 +1,10 @@
+CoInductive stream :=
+| C : content -> stream
+with content :=
+| D : nat -> stream -> content.
+
+Lemma one : stream.
+cofix c with (d : content).
+- constructor. apply d.
+- constructor. exact 1. apply c.
+Defined.