From edfda2501f08f18e24bd2e3eca763eb1c2dec0ea Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 18 Oct 2000 17:51:58 +0000
Subject: Simplifications autour de typed_type (renommé types par analogie avec
 sorts); documentation

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

(limited to 'proofs/refiner.ml')

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 868e71f850..495a9ca826 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -255,9 +255,8 @@ let extract_open_proof sigma pf =
 	       mkNamedProd_or_LetIn (id,c,ty) concl)
             sorted_rels goal.evar_concl
 	in
-	let ass = Retyping.get_assumption_of goal.evar_env sigma abs_concl in
 	let mv = new_meta() in
-	open_obligations := (mv,ass):: !open_obligations;
+	open_obligations := (mv,abs_concl):: !open_obligations;
 	applist (mkMeta mv, List.map (fun (n,_) -> mkRel n) sorted_rels) 
 	  
     | _ -> anomaly "Bug : a case has been forgotten in proof_extractor"
-- 
cgit v1.2.3