[declare] Fix types of mutual lemmas when using Admitted.

We fix a clear coding mistake in
79bcf1c0a22e736c4e2cae3460c35b3d9fca9aa0 that forgot to update the
type of the parameter entry when saving mutual definitions without a
body.

We follow the solution suggested by Hugo Herbelin and drop the
type used in `start_proof`. Note the duplication here indeed.

Fixes #12895

Co-authored-by: Hugo Herbelin <Hugo.Herbelin@inria.fr>

1 files changed, 20 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_12895.v b/test-suite/bugs/closed/bug_12895.v
new file mode 100644
index 0000000000..53adc2981c
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12895.v
@@ -0,0 +1,20 @@
+Fixpoint bug_1 (e1 : nat) {struct e1}
+  : nat
+with bug_2 {H_imp : nat} (e2 : nat) {struct e2}
+  : nat.
+Proof.
+  - exact e1.
+  - exact e2.
+Admitted.
+
+Fixpoint hbug_1 (a:bool) (e1 : nat) {struct e1}
+  : nat
+with hbug_2 (a:nat) (e2 : nat) {struct e2}
+  : nat.
+Proof.
+  - exact e1.
+  - exact e2.
+Admitted.
+
+Check (hbug_1 : bool -> nat -> nat).
+Check (hbug_2 : nat -> nat -> nat).