Fixing a small bug in computing implicit arguments in (co-)fixpoints.

The recursive functions and their binders were not pushed in the right
order for implicit arguments.

Additionally, we avoid calling push_name_env both for interpreting the
type of each component of a (co-)fixpoint and for interpreting again the
body of each component of a (co-)fixpoint because it may have
side-effects (in the glob file). So we instead remember the part of
its action on implicit arguments to replay it functionally.

1 files changed, 16 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_10197.v b/test-suite/bugs/closed/bug_10197.v
new file mode 100644
index 0000000000..920c5f5cb7
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10197.v
@@ -0,0 +1,16 @@
+(* Some check about implicit arguments in fix *)
+
+Check fix f {f:nat} := match f with 0 => true | _ => false end.
+
+CoInductive stream := { this : nat ; next : option stream }.
+
+Check cofix f {f:nat} := {| this := f ; next := None |}.
+
+(* The following was ok from 8.4, just checking that the order is not
+   mixed up accidentally *)
+
+Check fix f (x : nat) (x : forall {a:nat}, a = 0 -> nat) :=
+   match x eq_refl with 0 => true | _ => false end.
+
+Check fix f (x : forall {a:nat}, a = 0 -> bool) (x : nat) :=
+   match x with 0 => true | _ => false end.