diff options
| author | herbelin | 2007-05-29 10:01:06 +0000 |
|---|---|---|
| committer | herbelin | 2007-05-29 10:01:06 +0000 |
| commit | 28a551e49864bbfee8a9212fdbcc364d1132b19e (patch) | |
| tree | af54777193da1f6e12e60e295006c13cf5247f34 /tactics | |
| parent | 7b00173a3e2cb44162e6d90e9306b20621ad046b (diff) | |
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
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/contradiction.ml | 2 | ||||
| -rw-r--r-- | tactics/decl_proof_instr.ml | 2 | ||||
| -rw-r--r-- | tactics/equality.ml | 2 | ||||
| -rw-r--r-- | tactics/evar_tactics.ml | 4 |
4 files changed, 5 insertions, 5 deletions
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 |