Bug affichage des metas dans un environnement avec definitions locales (bug 277)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5116 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 6 deletions

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 489c3f5c0..575c27fbd 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -301,15 +301,16 @@ let extract_open_proof sigma pf =
             (ids_of_named_context goal.evar_hyps) in
 	let sorted_rels =
 	  Sort.list (fun (n1,_) (n2,_) -> n1 > n2 ) visible_rels in
+        let sorted_env =
+          List.map (fun (n,id) -> (n,Sign.lookup_named id goal.evar_hyps))
+            sorted_rels in
 	let abs_concl =
-          List.fold_right
-            (fun (_,id) concl ->
-	       let (_,c,ty) = Sign.lookup_named id goal.evar_hyps in
-	       mkNamedProd_or_LetIn (id,c,ty) concl)
-            sorted_rels goal.evar_concl	in
+          List.fold_right (fun (_,decl) c -> mkNamedProd_or_LetIn decl c)
+            sorted_env goal.evar_concl	in
+        let inst = List.filter (fun (_,(_,b,_)) -> b = None) sorted_env in
         let meta = next_meta () in
 	open_obligations := (meta,abs_concl):: !open_obligations;
-	applist (mkMeta meta, List.map (fun (n,_) -> mkRel n) sorted_rels) 
+	applist (mkMeta meta, List.map (fun (n,_) -> mkRel n) inst) 
 	  
     | _ -> anomaly "Bug : a case has been forgotten in proof_extractor"
   in