From 28a551e49864bbfee8a9212fdbcc364d1132b19e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 29 May 2007 10:01:06 +0000
Subject: Correction d'un bug dans l'affichage du message d'erreur real_clean
 (cas d'un terme sans Rel libre), introduction au passage d'un nouveau type
 d'evar EvarGoal pour raffinement du message d'erreur.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9868 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/contradiction.ml    | 2 +-
 tactics/decl_proof_instr.ml | 2 +-
 tactics/equality.ml         | 2 +-
 tactics/evar_tactics.ml     | 4 ++--
 4 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'tactics')

diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index d504773160..62ed700a27 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -24,7 +24,7 @@ open Rawterm
 let absurd c gls =
   let env = pf_env gls and sigma = project gls in
   let _,j = Coercion.Default.inh_coerce_to_sort dummy_loc env
-    (Evd.create_evar_defs sigma) (Retyping.get_judgment_of env sigma c) in
+    (Evd.create_goal_evar_defs sigma) (Retyping.get_judgment_of env sigma c) in
   let c = j.Environ.utj_val in
   (tclTHENS
      (tclTHEN (elim_type (build_coq_False ())) (cut c)) 
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 28fc640d12..74ffc0a9c8 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -83,7 +83,7 @@ Please \"suppose\" something or \"end\" it now."
       | _ -> ()
 
 let mk_evd metalist gls =
-  let evd0= create_evar_defs (sig_sig gls) in
+  let evd0= create_goal_evar_defs (sig_sig gls) in
   let add_one (meta,typ) evd = 
     meta_declare meta typ evd in
     List.fold_right add_one metalist evd0
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 8c87161109..c5b7aeedfb 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -650,7 +650,7 @@ let minimal_free_rels env sigma (c,cty) =
 
 let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
   let { intro = exist_term } = find_sigma_data sort_of_ty in 
-  let isevars = ref (Evd.create_evar_defs sigma) in
+  let isevars = ref (Evd.create_goal_evar_defs sigma) in
   let rec sigrec_clausal_form siglen p_i =
     if siglen = 0 then
       (* is the default value typable with the expected type *)
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index f3454b711b..784455ff0d 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -51,7 +51,7 @@ let instantiate n rawc ido gl =
       error "not enough uninstantiated existential variables";
     if n <= 0 then error "incorrect existential variable index";
     let ev,_ =  destEvar (List.nth evl (n-1)) in
-    let evd' = w_refine ev rawc (create_evar_defs sigma)  in
+    let evd' = w_refine ev rawc (create_goal_evar_defs sigma)  in
       Refiner.tclEVARS (evars_of evd') gl
 	
 (*
@@ -68,7 +68,7 @@ let instantiate_tac = function
 *)
 
 let let_evar name typ gls =
-  let evd = Evd.create_evar_defs gls.sigma in
+  let evd = Evd.create_goal_evar_defs gls.sigma in
   let evd',evar = Evarutil.new_evar evd (pf_env gls) typ in
   Refiner.tclTHEN (Refiner.tclEVARS (evars_of evd'))
     (Tactics.letin_tac true name evar nowhere) gls
-- 
cgit v1.2.3