Fix bug #931: leave dependent evars as such for refine

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

4 files changed, 37 insertions, 12 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index a49d8540b..5570763e1 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -101,20 +101,36 @@ let new_meta =
 
 let mk_new_meta () = mkMeta(new_meta())
 
+let collect_evars emap c =
+  let rec collrec acc c =
+    match kind_of_term c with
+      | Evar (k,_) when 
+	  Evd.in_dom emap k & not (Evd.is_defined emap k) -> k::acc
+      | _         ->
+	  fold_constr collrec acc c in
+  list_uniquize (collrec [] c)
+
+let push_dependent_evars sigma emap =
+  Evd.fold (fun ev {evar_concl = ccl} (sigma',emap') ->
+    List.fold_left 
+      (fun (sigma',emap') ev -> 
+	(Evd.add sigma' ev (Evd.map emap' ev),Evd.rmv emap' ev))
+      (sigma',emap') (collect_evars emap' ccl))
+    emap (sigma,emap)
+    
 (* replaces a mapping of existentials into a mapping of metas.
    Problem if an evar appears in the type of another one (pops anomaly) *)
-let exist_to_meta sigma (emap, c) =
-  let metamap = ref [] in
+let evars_to_metas sigma (emap, c) =
+  let sigma',emap' = push_dependent_evars sigma emap in
   let change_exist evar =
     let ty = nf_betaiota (nf_evar emap (existential_type emap evar)) in
     let n = new_meta() in
-    metamap := (n, ty) :: !metamap;
     mkCast (mkMeta n, ty) in
   let rec replace c =
     match kind_of_term c with
-        Evar (k,_ as ev) when not (Evd.in_dom sigma k) -> change_exist ev
+        Evar (k,_ as ev) when Evd.in_dom emap' k -> change_exist ev
       | _ -> map_constr replace c in
-  (!metamap, replace c)
+  (sigma', replace c)
 
 (*************************************)
 (* Metas *)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 1831110a7..e8669e5fa 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -61,9 +61,10 @@ val evar_define :
 (***********************************************************)
 (* Evars/Metas switching... *)
 
-(* [exist_to_meta] generates new metavariables for each existential
-   and performs the replacement in the given constr *)
-val exist_to_meta : evar_map -> open_constr -> (Termops.metamap * constr)
+(* [evars_to_metas] generates new metavariables for each non dependent
+   existential and performs the replacement in the given constr; it also
+   returns the evar_map extended with dependent evars *)
+val evars_to_metas : evar_map -> open_constr -> (evar_map * constr)
 
 val non_instantiated : evar_map -> (evar * evar_info) list
 
diff --git a/tactics/refine.ml b/tactics/refine.ml
index db4c52020..d53310c66 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -337,8 +337,8 @@ let rec tcc_aux subst (TH (c,mm,sgp) as th) gl =
 
 let refine oc gl =
   let sigma = project gl in
-  let (_gmm,c) = Evarutil.exist_to_meta sigma oc in
-  (* Relies on Cast's put on Meta's by exist_to_meta, because it is otherwise 
-     complicated to update gmm when passing through a binder *)
+  let (sigma,c) = Evarutil.evars_to_metas sigma oc in
+  (* Relies on Cast's put on Meta's by evars_to_metas, because it is otherwise 
+     complicated to update meta types when passing through a binder *)
   let th = compute_metamap (pf_env gl) c in
-  tcc_aux [] th gl
+  tclTHEN (Refiner.tclEVARS sigma) (tcc_aux [] th) gl
diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v
index 47453b9ca..96fa79ebd 100644
--- a/test-suite/success/refine.v
+++ b/test-suite/success/refine.v
@@ -53,3 +53,11 @@ Refine [n]
     Cases i of 0 => ? | (S _) => ? end }.
 Abort.
 
+(* Submitted by Roland Zumkeller (bug #931) *)
+(* Don't turn dependent evar into metas *)
+
+Goal ((n:nat)n=O->Prop) -> Prop.
+Intro P.
+Refine(P ? ?).
+Reflexivity.
+Abort.