From a2be2d34776d756c479b38b071d21f4b5c691cf3 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 24 Mar 2006 22:03:26 +0000
Subject: Patch envoy\'e par Benjamin Gregoire, permettant de corriger un
 probleme avec normalise_vm_in_concl

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

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 071e44b5be..59ff7a3224 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -627,7 +627,7 @@ let prim_extractor subfun vl pft =
     (* Structural and conversion rules do not produce any proof *)
     | Some (Prim (Convert_concl (t,k)),[pf]) ->
 	if k = DEFAULTcast then subfun vl pf
-	else mkCast (subfun vl pf,k,cl)
+	else mkCast (subfun vl pf,k,subst_proof_vars vl cl)
     | Some (Prim (Convert_hyp _),[pf]) ->
 	subfun vl pf
 
-- 
cgit v1.2.3