v8.3: Fixing critical bug in typing match with let-ins in the arity.

coq · Nov 23, 2015 · 4bed028 · 4bed028
1 parent a9461b3
commit 4bed028
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 1 deletion.
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
@@ -125,7 +125,7 @@ let betazeta_appvect n c v =
     if n = 0 then applist (substl env t, stack) else
     match kind_of_term t, stack with
         Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl
-      | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack
+      | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack
       | _ -> anomaly "Not enough lambda/let's" in
   stacklam n [] c (Array.to_list v)
 

diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v
@@ -0,0 +1,12 @@
+(* This wrongly succeeded in 8.3pl5 *)
+
+Inductive IND : forall X:Type, let Y:=X in Type :=
+  C : IND True.
+
+Definition F (x:IND True) (A:Type) :=
+  match x in IND Y Z return Z with
+  C => I
+  end.
+
+Theorem paradox : False.
+Fail Proof (F C False).