Correction du bug #1315:

- ajouts des opérations clear_evar_hyps_in_evar,
  clear_evar_hyps_in_constr et clear_evar_hyps dans Evarutil, qui
  permettent de supprimer des hypothèses dans le contexte des evars, 
  en créant une nouvelle evar avec un contexte restreint;

- adaptation de clear_hyps dans Logic pour qu'elle mette à jour le
  contexte des evars;

- adaptation de prim_refiner pour qu'elle renvoie le evar_map modifié;

- déplacement de la tactique Change_evars dans prim_rule.



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

1 files changed, 1 insertions, 11 deletions

diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml
index 5eedeec079..c2e0e27fb5 100644
--- a/parsing/tactic_printer.ml
+++ b/parsing/tactic_printer.ml
@@ -39,11 +39,6 @@ let pr_rule = function
       end
   | Daimon -> str "<Daimon>"
   | Decl_proof _ -> str "proof" 
-  | Change_evars ->
-      (* This is internal tactic and cannot be replayed at user-level.
-         Function pr_rule_dot below is used when we want to hide
-         Change_evars *)
-      str "Evar change"
 
 let uses_default_tac = function
   | Nested(Tactic(_,dflt),_) -> dflt
@@ -51,7 +46,7 @@ let uses_default_tac = function
 
 (* Does not print change of evars *)
 let pr_rule_dot = function 
-  | Change_evars -> mt ()
+  | Prim Change_evars -> mt ()
   | r ->
       pr_rule r ++ if uses_default_tac r then str "..." else str"."
 
@@ -189,9 +184,6 @@ let print_treescript nochange sigma pf =
 	((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++
 	   prlist_with_sep pr_fnl
            (print_script nochange sigma) spfl )
-    | Some(Change_evars,[spf]) ->
-        (if nochange then mt () else pr_change pf.goal ++ fnl ()) ++
-        aux spf
     | Some(r,spfl) ->
         let indent = if List.length spfl >= 2 then 1 else 0 in
         (if nochange then mt () else (pr_change pf.goal ++ fnl ())) ++
@@ -202,8 +194,6 @@ let rec print_info_script sigma osign pf =
   let {evar_hyps=sign; evar_concl=cl} = pf.goal in
   match pf.ref with
     | None -> (mt ())
-    | Some(Change_evars,[spf]) ->
-        print_info_script sigma osign spf
     | Some(r,spfl) ->
         (pr_rule r ++ 
            match spfl with