diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-11 20:01:04 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-11 20:01:04 +0000 |
| commit | 0601db38b579513e4ab39a161591cd359260490e (patch) | |
| tree | 2741c3b805ec8b890c5b9f58aeb1445ec10590fc /tactics | |
| parent | 8556f4e4b5e21535013e6962feabfede6313462b (diff) | |
Promote evar_defs to evar_map (in Evd)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12502 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/decl_proof_instr.ml | 2 | ||||
| -rw-r--r-- | tactics/equality.mli | 2 | ||||
| -rw-r--r-- | tactics/rewrite.ml4 | 6 | ||||
| -rw-r--r-- | tactics/tacinterp.mli | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
5 files changed, 7 insertions, 7 deletions
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index 8c47497a1..9c58f06ee 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -327,7 +327,7 @@ type stackd_elt = se_type:types; se_last_meta:metavariable; se_meta_list:(metavariable*types) list; - se_evd: evar_defs} + se_evd: evar_map} let rec replace_in_list m l = function [] -> raise Not_found diff --git a/tactics/equality.mli b/tactics/equality.mli index 8c43888fb..e79254ce2 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -49,7 +49,7 @@ val rewriteRL : ?tac:(tactic * conditions) -> constr -> tactic val register_general_rewrite_clause : (identifier option -> orientation -> occurrences -> open_constr with_bindings -> new_goals:constr list -> tactic) -> unit -val register_is_applied_rewrite_relation : (env -> evar_defs -> rel_context -> constr -> open_constr option) -> unit +val register_is_applied_rewrite_relation : (env -> evar_map -> rel_context -> constr -> open_constr option) -> unit val general_rewrite_ebindings_clause : identifier option -> orientation -> occurrences -> ?tac:(tactic * conditions) -> open_constr with_bindings -> evars_flag -> tactic diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index d3d488183..1ba25fc60 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -429,7 +429,7 @@ type rewrite_flags = { under_lambdas : bool; on_morphisms : bool } let default_flags = { under_lambdas = true; on_morphisms = true; } -type evars = evar_defs * evar_defs (* goal evars, constraint evars *) +type evars = evar_map * evar_map (* goal evars, constraint evars *) type rewrite_result_info = { rew_car : constr; @@ -442,7 +442,7 @@ type rewrite_result_info = { type rewrite_result = rewrite_result_info option -type strategy = Environ.env -> evar_defs -> constr -> types -> +type strategy = Environ.env -> evar_map -> constr -> types -> constr option -> evars -> rewrite_result option let resolve_subrelation env sigma car rel rel' res = @@ -525,7 +525,7 @@ let apply_rule hypinfo loccs : strategy = | Some (env', (prf, (car, rel, c1, c2))) when is_occ !occ -> begin let goalevars = Evd.evar_merge (fst evars) - (Evd.undefined_evars (Evarutil.nf_evar_defs env'.evd)) + (Evd.undefined_evars (Evarutil.nf_evar_map env'.evd)) in let res = { rew_car = ty; rew_rel = rel; rew_from = c1; rew_to = c2; rew_prf = prf; rew_evars = goalevars, snd evars } diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 307e3a97d..ce8cfa7db 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -43,7 +43,7 @@ and interp_sign = debug : debug_info; trace : ltac_trace } -val extract_ltac_vars : interp_sign -> Evd.evar_defs -> Environ.env -> +val extract_ltac_vars : interp_sign -> Evd.evar_map -> Environ.env -> Pretyping.var_map * Pretyping.unbound_ltac_var_map (* Transforms an id into a constr if possible *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 48e45e8d8..70e8557db 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -887,7 +887,7 @@ let check_evars sigma evm gl = if rest <> Evd.empty then errorlabstrm "apply" (str"Uninstantiated existential "++ str(plural (List.length (Evd.to_list rest)) "variable")++str": " ++ - fnl () ++ pr_evar_defs rest);; + fnl () ++ pr_evar_map rest);; let get_bindings_evars = function | ImplicitBindings largs -> List.map fst largs |