From 90a2cea28df5ecdf9e2cdc4351aad5f6a993a003 Mon Sep 17 00:00:00 2001
From: notin
Date: Mon, 22 Jan 2007 18:06:35 +0000
Subject: 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
---
 tactics/decl_proof_instr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 244cb288e2..4ac92fbaed 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -54,7 +54,7 @@ let tcl_change_info_gen info_gen =
       [pftree] ->
 	{pftree with
 	   goal=gl;
-	   ref=Some (Change_evars,[pftree])} 
+	   ref=Some (Prim Change_evars,[pftree])} 
     | _ -> anomaly "change_info : Wrong number of subtrees")
 
 let tcl_change_info info gls =  tcl_change_info_gen (Some (pm_in info)) gls
-- 
cgit v1.2.3