From 729b9a0a10eec0c67680b738ca52b4e85cb23f1b Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 13 Mar 2011 17:35:47 +0000
Subject: Fix inductive_template building ill-typed evars, and update
 test-suite scripts

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

(limited to 'pretyping')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 5e2c0729c8..331cd01231 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -313,7 +313,7 @@ let inductive_template evdref env tmloc ind =
 	    let e = e_new_evar evdref env ~src:(hole_source n) ty' in
 	    (e::subst,e::evarl,n+1)
 	| Some b ->
-	    (b::subst,evarl,n+1))
+	    (substl subst b::subst,evarl,n+1))
       arsign ([],[],1) in
    applist (mkInd ind,List.rev evarl)
 
-- 
cgit v1.2.3