From 93b759f35a9f6544c5da9643330beb54ce255619 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 16 Nov 2011 08:46:46 +0000
Subject: Old typing bug in pattern-matching compilation (apparently w/o
 consequences up to now, but maybe because this type is often later on thrown
 away).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14663 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/cases.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 3fb7009564..932138f304 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1233,7 +1233,7 @@ and match_current pb tomatch =
 	  Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred;
 	  let inst = List.map mkRel deps in
 	  { uj_val = applist (case, inst);
-	    uj_type = substl inst typ }
+	    uj_type = prod_applist typ inst }
 
 and compile_branch current names deps pb arsign eqn cstr =
   let sign, pb = build_branch current deps names pb arsign eqn cstr in
-- 
cgit v1.2.3