Fixing a bug of adjust_subst_to_rel_context.

2 files changed, 16 insertions, 4 deletions

diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 5a55d47fd1..ebd9d939aa 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -930,7 +930,7 @@ let adjust_subst_to_rel_context sign l =
     match sign, l with
     | (_,None,_)::sign', a::args' -> aux (a::subst) sign' args'
     | (_,Some c,_)::sign', args' ->
-	aux (substl (List.rev subst) c :: subst) sign' args'
+	aux (substl subst c :: subst) sign' args'
     | [], [] -> List.rev subst
     | _ -> anomaly (Pp.str "Instance and signature do not match")
   in aux [] (List.rev sign) l
diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v
index 8c8f02eccf..f88051f8f5 100644
--- a/test-suite/success/Case22.v
+++ b/test-suite/success/Case22.v
@@ -30,14 +30,26 @@ Check fun x:I2 nat nat => match x in I2 _ X Y Z return X*Y*Z with
 (* This used to succeed in 8.3, 8.4 and 8.5beta1 *)
 
 Inductive IND : forall X:Type, let Y:=X in Type :=
-  C : IND True.
+  CONSTR : IND True.
 
 Definition F (x:IND True) (A:Type) :=
   (* This failed in 8.5beta2 though it should have been accepted *)
-  match x in IND Y Z return Z with
-  C => I
+  match x in IND X Y return Y with
+  CONSTR => Logic.I
   end.
 
 Theorem paradox : False.
   (* This succeeded in 8.3, 8.4 and 8.5beta1 because F had wrong type *)
 Fail Proof (F C False).
+
+(* Another bug found in November 2015 (a substitution was wrongly
+   reversed at pretyping level) *)
+
+Inductive Ind (A:Type) :
+  let X:=A in forall Y:Type, let Z:=(X*Y)%type in Type :=
+  Constr : Ind A nat.
+
+Check fun x:Ind bool nat =>
+  match x in Ind _ X Y Z return Z with
+  | Constr _ => (true,0)
+  end.