From e5a040666d1dc58995d7a08e8fe18de90abc7a2d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 25 Nov 1999 01:13:00 +0000
Subject: Backtrack sur modif Evd.evd_concl

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

(limited to 'proofs/proof_trees.ml')

diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index a119354a01..3523f42182 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -96,8 +96,7 @@ let lc_toList lc = Intset.elements lc
 (* Functions on goals *)
 
 let mk_goal ctxt env cl = 
-  let ty = execute_type env Evd.empty cl in
-  { evar_env = env; evar_concl = ty; evar_body = Evar_empty; evar_info = ctxt }
+  { evar_env = env; evar_concl = cl; evar_body = Evar_empty; evar_info = ctxt }
 
 (* Functions on the information associated with existential variables  *)
 
-- 
cgit v1.2.3