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

5 files changed, 166 insertions, 168 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index f56a924756..57b5d677f1 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -69,26 +69,37 @@ let with_check = Options.with_option check
 (* The Clear tactic: it scans the context for hypotheses to be removed
    (instead of iterating on the list of identifier to be removed, which
    forces the user to give them in order). *)
-let clear_hyps ids gl =
+let clear_hyps sigma ids gl =
   let env = Global.env() in
-  let (nhyps,cleared_ids) =
-    let fcheck cleared_ids (id,_,_ as d)  =
-      if !check && cleared_ids<>[] then
-	Idset.iter
-	  (fun id' ->
-            if List.mem id' cleared_ids then
-              error (string_of_id id'^
-		        " is used in hypothesis "^string_of_id id))
-	  (global_vars_set_of_decl env d) in
-      clear_hyps ids fcheck gl.evar_hyps in
-  let ncl = gl.evar_concl in
+  let evd = ref (Evd.create_evar_defs sigma) in
+  let (nhyps, cleared_ids) = 
+    let check_and_clear_in_evar_hyps (id,ob,c) = 
+      let rec aux c =
+	match kind_of_term c with
+	  | (Rel _ | Meta _ | Sort _ | Const _ | Ind _
+	    | Construct _) -> c
+	  | Var id' ->  if !check && List.mem id' ids then
+		error (string_of_id id' ^ " is used in hypothesis "
+			^ string_of_id id); mkVar id'
+	  | Evar (e,l) -> 
+	      (* If e is already define, we replace it by its definition *)
+	      if Evd.is_defined_evar !evd (e,l) then
+		let nc = nf_evar (evars_of !evd) c in aux nc
+	      else
+		Evarutil.clear_evar_hyps_in_evar evd e l ids
+	  | _ -> map_constr aux c
+      in
+	(id, (match ob with None -> None | Some b -> Some (aux b)), aux c)
+    in
+      remove_hyps ids check_and_clear_in_evar_hyps (evar_hyps gl) in
+  let ncl = Evarutil.clear_evar_hyps_in_constr evd (evar_concl gl) ids in
     if !check && cleared_ids<>[] then
       Idset.iter
 	(fun id' ->
           if List.mem id' cleared_ids then
             error (string_of_id id'^" is used in conclusion"))
-	(global_vars_set_drop_evar env ncl);
-    mk_goal nhyps ncl gl.evar_extra
+	(global_vars_set env ncl);
+    (mk_goal nhyps ncl gl.evar_extra, evars_of !evd)
 
 (* The ClearBody tactic *)
 
@@ -216,7 +227,7 @@ let check_forward_dependencies id tail =
 
 let check_goal_dependency id cl =
   let env = Global.env() in
-    if Idset.mem id (global_vars_set_drop_evar env cl) then
+    if Idset.mem id (global_vars_set env cl) then
       error (string_of_id id^" is used in conclusion")
 
 let rename_hyp id1 id2 sign =
@@ -398,6 +409,19 @@ let convert_hyp sign sigma (id,b,bt as d) =
 	 error ("Incorrect change of the body of "^(string_of_id id));
        d)
 
+(* Normalizing evars in a goal. Called by tactic Local_constraints
+   (i.e. when the sigma of the proof tree changes). Detect if the
+   goal is unchanged *)
+let norm_goal sigma gl =
+  let red_fun = Evarutil.nf_evar sigma in
+  let ncl = red_fun gl.evar_concl in
+  let ngl =
+    { gl with 
+	evar_concl = ncl;
+	evar_hyps = map_named_val red_fun gl.evar_hyps } in
+    if Evd.eq_evar_info ngl gl then None else Some ngl
+
+
 
 (************************************************************************)
 (************************************************************************)
@@ -418,13 +442,13 @@ let prim_refiner r sigma goal =
 	       if occur_meta c1 then error_use_instantiate();
 	       let sg = mk_goal (push_named_context_val (id,None,c1) sign)
 			  (subst1 (mkVar id) b) in
-	       [sg]
+	       ([sg], sigma)
 	   | LetIn (_,c1,t1,b) ->
 	       if occur_meta c1 or occur_meta t1 then error_use_instantiate();
 	       let sg =
 		 mk_goal (push_named_context_val (id,Some c1,t1) sign)
 		   (subst1 (mkVar id) b) in
-	       [sg]
+	       ([sg], sigma)
 	   | _ ->
 	       raise (RefinerError IntroNeedsProduct))
 	
@@ -434,12 +458,12 @@ let prim_refiner r sigma goal =
 	       if occur_meta c1 then error_use_instantiate();
 	       let sign' = replace_hyp sign id (id,None,c1) cl in
 	       let sg = mk_goal sign' (subst1 (mkVar id) b) in
-	       [sg]
+	       ([sg], sigma)
            | LetIn (_,c1,t1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
 	       let sign' = replace_hyp sign id (id,Some c1,t1) cl in
 	       let sg = mk_goal sign' (subst1 (mkVar id) b) in
-	       [sg]
+	       ([sg], sigma)
 	   | _ ->
 	       raise (RefinerError IntroNeedsProduct))
 	
@@ -449,7 +473,7 @@ let prim_refiner r sigma goal =
         if occur_meta t then error_use_instantiate();
         let sg1 = mk_goal sign (nf_betaiota t) in
         let sg2 = mk_goal (push_named_context_val (id,None,t) sign) cl in
-        if b then [sg1;sg2] else [sg2;sg1]  
+        if b then ([sg1;sg2],sigma) else ([sg2;sg1], sigma)
 
     | FixRule (f,n,rest) ->
      	let rec check_ind env k cl = 
@@ -478,7 +502,7 @@ let prim_refiner r sigma goal =
 	  | [] -> 
 	      List.map (fun (_,_,c) -> mk_goal sign c) all
 	in 
-	mk_sign sign all
+	  (mk_sign sign all, sigma)
 	
     | Cofix (f,others) ->
      	let rec check_is_coind env cl = 
@@ -505,47 +529,48 @@ e types")
                   mk_sign (push_named_context_val (f,None,ar) sign) oth)
 	  | [] -> List.map (fun (_,c) -> mk_goal sign c) all
      	in 
-	mk_sign sign all
+	  (mk_sign sign all, sigma)
 
     | Refine c ->
         if not (list_distinct (collect_meta_variables c)) then
           raise (RefinerError (NonLinearProof c));
 	let (sgl,cl') = mk_refgoals sigma goal [] cl c in
 	let sgl = List.rev sgl in
-	sgl
+	  (sgl, sigma)
 
     (* Conversion rules *)
     | Convert_concl (cl',_) ->
 	check_typability env sigma cl';
 	if (not !check) || is_conv_leq env sigma cl' cl then
           let sg = mk_goal sign cl' in
-          [sg]
+          ([sg], sigma)
 	else 
 	  error "convert-concl rule passed non-converting term"
 
     | Convert_hyp (id,copt,ty) ->
-	[mk_goal (convert_hyp sign sigma (id,copt,ty)) cl]
+	([mk_goal (convert_hyp sign sigma (id,copt,ty)) cl], sigma)
 
     (* And now the structural rules *)
     | Thin ids -> 
-	[clear_hyps ids goal]
-
+	let (ngl, nsigma) = clear_hyps sigma ids goal in
+	  ([ngl], nsigma)
+	
     | ThinBody ids ->
 	let clear_aux env id =
           let env' = remove_hyp_body env sigma id in
-          if !check then recheck_typability (None,id) env' sigma cl;
-          env'
+            if !check then recheck_typability (None,id) env' sigma cl;
+            env'
 	in
 	let sign' = named_context_val (List.fold_left clear_aux env ids) in
      	let sg = mk_goal sign' cl in
-     	[sg]
+     	  ([sg], sigma)
 
     | Move (withdep, hfrom, hto) ->
   	let (left,right,declfrom,toleft) = 
 	  split_sign hfrom hto (named_context_of_val sign) in
   	let hyps' = 
 	  move_after withdep toleft (left,declfrom,right) hto in
-  	[mk_goal hyps' cl]
+  	  ([mk_goal hyps' cl], sigma)
 
     | Rename (id1,id2) ->
         if !check & id1 <> id2 &&
@@ -553,7 +578,12 @@ e types")
           error ((string_of_id id2)^" is already used");
         let sign' = rename_hyp id1 id2 sign in
         let cl' = replace_vars [id1,mkVar id2] cl in
-        [mk_goal sign' cl']
+          ([mk_goal sign' cl'], sigma)
+
+    | Change_evars as r ->
+        match norm_goal sigma goal with
+	    Some ngl -> ([ngl],sigma)
+          | None -> ([goal], sigma)
 
 (************************************************************************)
 (************************************************************************)
@@ -596,80 +626,83 @@ let proof_variable_index x =
 
 let prim_extractor subfun vl pft =
   let cl = pft.goal.evar_concl in
-  match pft.ref with
-    | Some (Prim (Intro id), [spf]) ->
-	(match kind_of_term (strip_outer_cast cl) with
-	   | Prod (_,ty,_) ->
-	       let cty = subst_proof_vars vl ty in
-	       mkLambda (Name id, cty, subfun (add_proof_var id vl) spf)
-	   | LetIn (_,b,ty,_) ->
-	       let cb = subst_proof_vars vl b in
-	       let cty = subst_proof_vars vl ty in
-	       mkLetIn (Name id, cb, cty, subfun (add_proof_var id vl) spf)
-	   | _ -> error "incomplete proof!")
-	
-    | Some (Prim (Intro_replacing id),[spf]) ->
-	(match kind_of_term (strip_outer_cast cl) with
-	   | Prod (_,ty,_) ->
-	       let cty = subst_proof_vars vl ty in
-	       mkLambda (Name id, cty, subfun (add_proof_var id vl) spf)
-	   | LetIn (_,b,ty,_) ->
-	       let cb = subst_proof_vars vl b in
-	       let cty = subst_proof_vars vl ty in
-	       mkLetIn (Name id, cb, cty, subfun (add_proof_var id vl) spf)
-	   | _ -> error "incomplete proof!")
-
-    | Some (Prim (Cut (b,id,t)),[spf1;spf2]) ->
-        let spf1, spf2 = if b then spf1, spf2 else spf2, spf1 in
-	mkLetIn (Name id,subfun vl spf1,subst_proof_vars vl t,
-                 subfun (add_proof_var id vl) spf2)
-
-    | Some (Prim (FixRule (f,n,others)),spfl) ->
-	let all = Array.of_list ((f,n,cl)::others) in
-	let lcty = Array.map (fun (_,_,ar) -> subst_proof_vars vl ar) all in
-	let names = Array.map (fun (f,_,_) -> Name f) all in
-	let vn = Array.map (fun (_,n,_) -> n-1) all in
-	let newvl = List.fold_left (fun vl (id,_,_) -> add_proof_var id vl)
-          (add_proof_var f vl) others in
-	let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
-	mkFix ((vn,0),(names,lcty,lfix))	
-
-    | Some (Prim (Cofix (f,others)),spfl) ->
-	let all = Array.of_list ((f,cl)::others) in
-	let lcty = Array.map (fun (_,ar) -> subst_proof_vars vl ar) all in
-	let names  = Array.map (fun (f,_) -> Name f) all in
-	let newvl = List.fold_left (fun vl (id,_)-> add_proof_var id vl)
-          (add_proof_var f vl) others in 
-	let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
-	mkCoFix (0,(names,lcty,lfix))
-	  
-    | Some (Prim (Refine c),spfl) ->
-	let mvl = collect_meta_variables c in
-	let metamap = List.combine mvl (List.map (subfun vl) spfl) in
-	let cc = subst_proof_vars vl c in 
-	plain_instance metamap cc
-
-    (* Structural and conversion rules do not produce any proof *)
-    | Some (Prim (Convert_concl (t,k)),[pf]) ->
-	if k = DEFAULTcast then subfun vl pf
-	else mkCast (subfun vl pf,k,subst_proof_vars vl cl)
-    | Some (Prim (Convert_hyp _),[pf]) ->
-	subfun vl pf
-
-    | Some (Prim (Thin _),[pf]) ->
-     (* No need to make ids Anon in vl: subst_proof_vars take the most recent*)
-	subfun vl pf
-	
-    | Some (Prim (ThinBody _),[pf]) ->
-	subfun vl pf
-	
-    | Some (Prim (Move _),[pf]) ->
-	subfun vl pf
-
-    | Some (Prim (Rename (id1,id2)),[pf]) ->
-	subfun (rebind id1 id2 vl) pf
-
-    | Some _ -> anomaly "prim_extractor"
-
-    | None-> error "prim_extractor handed incomplete proof"
+    match pft.ref with
+      | Some (Prim (Intro id), [spf]) ->
+	  (match kind_of_term (strip_outer_cast cl) with
+	    | Prod (_,ty,_) ->
+		let cty = subst_proof_vars vl ty in
+		  mkLambda (Name id, cty, subfun (add_proof_var id vl) spf)
+	    | LetIn (_,b,ty,_) ->
+		let cb = subst_proof_vars vl b in
+		let cty = subst_proof_vars vl ty in
+		  mkLetIn (Name id, cb, cty, subfun (add_proof_var id vl) spf)
+	    | _ -> error "incomplete proof!")
+	    
+      | Some (Prim (Intro_replacing id),[spf]) ->
+	  (match kind_of_term (strip_outer_cast cl) with
+	    | Prod (_,ty,_) ->
+		let cty = subst_proof_vars vl ty in
+		  mkLambda (Name id, cty, subfun (add_proof_var id vl) spf)
+	    | LetIn (_,b,ty,_) ->
+		let cb = subst_proof_vars vl b in
+		let cty = subst_proof_vars vl ty in
+		  mkLetIn (Name id, cb, cty, subfun (add_proof_var id vl) spf)
+	    | _ -> error "incomplete proof!")
+
+      | Some (Prim (Cut (b,id,t)),[spf1;spf2]) ->
+          let spf1, spf2 = if b then spf1, spf2 else spf2, spf1 in
+	    mkLetIn (Name id,subfun vl spf1,subst_proof_vars vl t,
+                    subfun (add_proof_var id vl) spf2)
+
+      | Some (Prim (FixRule (f,n,others)),spfl) ->
+	  let all = Array.of_list ((f,n,cl)::others) in
+	  let lcty = Array.map (fun (_,_,ar) -> subst_proof_vars vl ar) all in
+	  let names = Array.map (fun (f,_,_) -> Name f) all in
+	  let vn = Array.map (fun (_,n,_) -> n-1) all in
+	  let newvl = List.fold_left (fun vl (id,_,_) -> add_proof_var id vl)
+            (add_proof_var f vl) others in
+	  let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
+	    mkFix ((vn,0),(names,lcty,lfix))	
+
+      | Some (Prim (Cofix (f,others)),spfl) ->
+	  let all = Array.of_list ((f,cl)::others) in
+	  let lcty = Array.map (fun (_,ar) -> subst_proof_vars vl ar) all in
+	  let names  = Array.map (fun (f,_) -> Name f) all in
+	  let newvl = List.fold_left (fun vl (id,_)-> add_proof_var id vl)
+            (add_proof_var f vl) others in 
+	  let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
+	    mkCoFix (0,(names,lcty,lfix))
+	      
+      | Some (Prim (Refine c),spfl) ->
+	  let mvl = collect_meta_variables c in
+	  let metamap = List.combine mvl (List.map (subfun vl) spfl) in
+	  let cc = subst_proof_vars vl c in 
+	    plain_instance metamap cc
+
+      (* Structural and conversion rules do not produce any proof *)
+      | Some (Prim (Convert_concl (t,k)),[pf]) ->
+	  if k = DEFAULTcast then subfun vl pf
+	  else mkCast (subfun vl pf,k,subst_proof_vars vl cl)
+      | Some (Prim (Convert_hyp _),[pf]) ->
+	  subfun vl pf
+
+      | Some (Prim (Thin _),[pf]) ->
+	  (* No need to make ids Anon in vl: subst_proof_vars take the most recent*)
+	  subfun vl pf
+	    
+      | Some (Prim (ThinBody _),[pf]) ->
+	  subfun vl pf
+	    
+      | Some (Prim (Move _),[pf]) ->
+	  subfun vl pf
+
+      | Some (Prim (Rename (id1,id2)),[pf]) ->
+	  subfun (rebind id1 id2 vl) pf
+
+      | Some (Prim Change_evars, [pf]) ->
+	  subfun vl pf
+
+      | Some _ -> anomaly "prim_extractor"
+
+      | None-> error "prim_extractor handed incomplete proof"
 	  
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 4af70cfb72..081d02f37e 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -34,7 +34,7 @@ val with_check    : tactic -> tactic
 
 (* The primitive refiner. *)
 
-val prim_refiner : prim_rule -> evar_map -> goal -> goal list
+val prim_refiner : prim_rule -> evar_map -> goal -> goal list * evar_map
 
 type proof_variable
 
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 5c9d2406ed..20ce39775c 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -39,6 +39,7 @@ type prim_rule =
   | ThinBody of identifier list
   | Move of bool * identifier * identifier
   | Rename of identifier * identifier
+  | Change_evars
 
 type proof_tree = {
   open_subgoals : int;
@@ -50,7 +51,6 @@ and rule =
   | Nested of compound_rule * proof_tree 
   | Decl_proof of bool
   | Daimon
-  | Change_evars
 
 and compound_rule=  
   | Tactic of tactic_expr * bool
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 9c82239ef3..f835e2ef42 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -39,6 +39,7 @@ type prim_rule =
   | ThinBody of identifier list
   | Move of bool * identifier * identifier
   | Rename of identifier * identifier
+  | Change_evars
 
 (* The type [goal sigma] is the type of subgoal. It has the following form
 \begin{verbatim}
@@ -84,7 +85,6 @@ and rule =
   | Nested of compound_rule * proof_tree 
   | Decl_proof of bool
   | Daimon
-  | Change_evars
 
 and compound_rule= 
   (* the boolean of Tactic tells if the default tactic is used *)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index ff74d89d30..a03e0b9e69 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -68,18 +68,6 @@ let descend n p =
     	else 
 	  error "Too few subproofs"
 
-(* Normalizing evars in a goal. Called by tactic Local_constraints
-   (i.e. when the sigma of the proof tree changes). Detect if the
-   goal is unchanged *)
-let norm_goal sigma gl =
-  let red_fun = Evarutil.nf_evar sigma in
-  let ncl = red_fun gl.evar_concl in
-  let ngl =
-    { gl with 
-	evar_concl = ncl;
-	evar_hyps = map_named_val red_fun gl.evar_hyps } in
-    if Evd.eq_evar_info ngl gl then None else Some ngl
-
 
 (* [mapshape [ l1 ; ... ; lk ] [ v1 ; ... ; vk ] [ p_1 ; .... ; p_(l1+...+lk) ]]
    gives
@@ -192,11 +180,11 @@ let abstract_operation syntax semantics gls =
   let (sgl_sigma,validation) = semantics gls in
   let hidden_proof = validation (List.map leaf sgl_sigma.it) in
   (sgl_sigma,
-   fun spfl ->
-     assert (check_subproof_connection sgl_sigma.it spfl);
-     { open_subgoals = and_status (List.map pf_status spfl);
-       goal = gls.it;
-       ref = Some(Nested(syntax,hidden_proof),spfl)})
+  fun spfl ->
+    assert (check_subproof_connection sgl_sigma.it spfl);
+    { open_subgoals = and_status (List.map pf_status spfl);
+      goal = gls.it;
+      ref = Some(Nested(syntax,hidden_proof),spfl)})
 
 let abstract_tactic_expr ?(dflt=false) te tacfun gls =
   abstract_operation (Tactic(te,dflt)) tacfun gls	
@@ -210,14 +198,14 @@ let abstract_extended_tactic ?(dflt=false) s args =
 let refiner = function
   | Prim pr as r ->
       let prim_fun = prim_refiner pr in
-      (fun goal_sigma ->
-         let sgl = prim_fun goal_sigma.sigma goal_sigma.it in 
-	 ({it=sgl; sigma = goal_sigma.sigma},
-          (fun spfl ->
-	     assert (check_subproof_connection sgl spfl);
-             { open_subgoals = and_status (List.map pf_status spfl);
-               goal = goal_sigma.it;
-               ref = Some(r,spfl) })))
+	(fun goal_sigma ->
+          let (sgl,sigma') = prim_fun goal_sigma.sigma goal_sigma.it in 
+	    ({it=sgl; sigma = sigma'},
+            (fun spfl ->
+	      assert (check_subproof_connection sgl spfl);
+              { open_subgoals = and_status (List.map pf_status spfl);
+		goal = goal_sigma.it;
+		ref = Some(r,spfl) })))
 
 
   | Nested (_,_) | Decl_proof _ -> 
@@ -234,44 +222,23 @@ let refiner = function
              goal = gls.it;
              ref = Some(Daimon,[])})
 
-   (* [Local_constraints lc] makes the local constraints be [lc] and
-      normalizes evars *)
-
-  | Change_evars as r ->
-      (fun goal_sigma ->
-         let gl = goal_sigma.it in
-         (match norm_goal goal_sigma.sigma gl with
-             Some ngl ->
-	       ({it=[ngl];sigma=goal_sigma.sigma},
-                (fun spfl -> 
-	          assert (check_subproof_connection [ngl] spfl);
-                  { open_subgoals = (List.hd spfl).open_subgoals;
-                    goal = gl;
-                    ref = Some(r,spfl) }))
-           (* if the evar change does not affect the goal, leave the
-              proof tree unchanged *)
-           | None -> ({it=[gl];sigma=goal_sigma.sigma},
-                      (fun spfl ->
-                        assert (List.length spfl = 1);
-                        List.hd spfl))))
-
-
-let local_Constraints gl = refiner Change_evars gl
+
+let local_Constraints gl = refiner (Prim Change_evars) gl
 
 let norm_evar_tac = local_Constraints
 
 let norm_evar_proof sigma pf =
   let nf_subgoal i sgl =
     let (gll,v) = norm_evar_tac {it=sgl.goal;sigma=sigma} in
-    v (List.map leaf gll.it) in
-  frontier_mapi nf_subgoal pf
+      v (List.map leaf gll.it) in
+    frontier_mapi nf_subgoal pf
 
 (* [extract_open_proof : proof_tree -> constr * (int * constr) list]
-  takes a (not necessarly complete) proof and gives a pair (pfterm,obl)
-  where pfterm is the constr corresponding to the proof
-  and [obl] is an [int*constr list] [ (m1,c1) ; ... ; (mn,cn)]
-  where the mi are metavariables numbers, and ci are their types.
-  Their proof should be completed in order to complete the initial proof *)
+   takes a (not necessarly complete) proof and gives a pair (pfterm,obl)
+   where pfterm is the constr corresponding to the proof
+   and [obl] is an [int*constr list] [ (m1,c1) ; ... ; (mn,cn)]
+   where the mi are metavariables numbers, and ci are their types.
+   Their proof should be completed in order to complete the initial proof *)
 
 let extract_open_proof sigma pf =
   let next_meta = 
@@ -291,8 +258,6 @@ let extract_open_proof sigma pf =
 	let flat_proof = v spfl in
 	proof_extractor vl flat_proof
  
-    | {ref=Some(Change_evars,[pf])} -> (proof_extractor vl) pf
-
     | {ref=Some(Decl_proof _,[pf])} -> (proof_extractor vl) pf
 	  
     | {ref=(None|Some(Daimon,[]));goal=goal} ->