Fixed bug #2930: folded let-in's were hiding a violation to the occur

check condition in pattern-unification, resulting in the instantiation
of evars by terms depending on themselves, henceforth leading
eventually to a stack overflow. Occur-check in the arguments of evars
was also missing.

[Also fixed what looked like a typo in the env passed to
project_evar_on_evar on line 1611.]

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15996 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/2930.v b/test-suite/bugs/closed/2930.v
new file mode 100644
index 000000000..0994b6fb2
--- /dev/null
+++ b/test-suite/bugs/closed/2930.v
@@ -0,0 +1,12 @@
+(* Checking that let-in's hiding evars are expanded when enforcing
+   "occur-check" *)
+
+Require Import List.
+
+Definition foo x y :=
+let xy := (x, y) in
+let bar xys  :=
+      match xys with
+      | nil => xy :: nil
+      | xy' :: xys' => xy' :: xys'
+      end in bar (nil : list (nat * nat)).