diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 2 | ||||
| -rw-r--r-- | proofs/goal.ml | 4 | ||||
| -rw-r--r-- | proofs/logic.ml | 1 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 1 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 2 | ||||
| -rw-r--r-- | proofs/proof_type.ml | 4 | ||||
| -rw-r--r-- | proofs/proof_type.mli | 4 | ||||
| -rw-r--r-- | proofs/proofview.ml | 2 | ||||
| -rw-r--r-- | proofs/refiner.ml | 5 | ||||
| -rw-r--r-- | proofs/tactic_debug.mli | 4 |
10 files changed, 13 insertions, 16 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 23a21414d8..fb1900f2f6 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -320,7 +320,7 @@ let clenv_pose_metas_as_evars clenv dep_mvs = if occur_meta ty then fold clenv (mvs@[mv]) else let (evd,evar) = - new_evar clenv.evd (cl_env clenv) ~src:(dummy_loc,Evar_kinds.GoalEvar) ty in + new_evar clenv.evd (cl_env clenv) ~src:(Loc.ghost,Evar_kinds.GoalEvar) ty in let clenv = clenv_assign mv evar {clenv with evd=evd} in fold clenv mvs in fold clenv dep_mvs diff --git a/proofs/goal.ml b/proofs/goal.ml index 9b3e901981..e7a6bce6cd 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -154,7 +154,7 @@ module Refinable = struct let my_type = Retyping.get_type_of env !rdefs t in let j = Environ.make_judge t my_type in let (new_defs,j') = - Coercion.inh_conv_coerce_to (Pp.dummy_loc) env !rdefs j typ + Coercion.inh_conv_coerce_to (Loc.ghost) env !rdefs j typ in rdefs := new_defs; j'.Environ.uj_val @@ -498,7 +498,7 @@ module V82 = struct Evd.evar_filter = List.map (fun _ -> true) (Environ.named_context_of_val hyps); Evd.evar_body = Evd.Evar_empty; - Evd.evar_source = (Pp.dummy_loc,Evar_kinds.GoalEvar); + Evd.evar_source = (Loc.ghost,Evar_kinds.GoalEvar); Evd.evar_candidates = None; Evd.evar_extra = extra } in diff --git a/proofs/logic.ml b/proofs/logic.ml index 3a5d2139b7..8247481e07 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Compat open Pp open Errors open Util diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 583e40c00b..60d24a50c5 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Loc open Pp open Names open Term diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 8dbb63739f..c394ab35bf 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -35,7 +35,7 @@ val check_no_pending_proof : unit -> unit val get_current_proof_name : unit -> Names.identifier val get_all_proof_names : unit -> Names.identifier list -val discard : Names.identifier Pp.located -> unit +val discard : Names.identifier Loc.located -> unit val discard_current : unit -> unit val discard_all : unit -> unit diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 61e89ac1dc..c4325fa54b 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -98,8 +98,8 @@ type ltac_call_kind = | LtacConstrInterp of glob_constr * (extended_patvar_map * (identifier * identifier option) list) -type ltac_trace = (int * loc * ltac_call_kind) list +type ltac_trace = (int * Loc.t * ltac_call_kind) list -exception LtacLocated of (int * ltac_call_kind * ltac_trace * loc) * exn +exception LtacLocated of (int * ltac_call_kind * ltac_trace * Loc.t) * exn let abstract_tactic_box = ref (ref None) diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 3476eaaabe..ac29fa877a 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -128,8 +128,8 @@ type ltac_call_kind = | LtacConstrInterp of glob_constr * (extended_patvar_map * (identifier * identifier option) list) -type ltac_trace = (int * loc * ltac_call_kind) list +type ltac_trace = (int * Loc.t * ltac_call_kind) list -exception LtacLocated of (int * ltac_call_kind * ltac_trace * loc) * exn +exception LtacLocated of (int * ltac_call_kind * ltac_trace * Loc.t) * exn val abstract_tactic_box : atomic_tactic_expr option ref ref diff --git a/proofs/proofview.ml b/proofs/proofview.ml index ff0e8de413..fc752cd336 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Compat - (* The proofview datastructure is a pure datastructure underlying the notion of proof (namely, a proof is a proofview which can evolve and has safety mechanisms attached). diff --git a/proofs/refiner.ml b/proofs/refiner.ml index cb588af2d3..dc58abbb24 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Compat open Pp open Errors open Util @@ -38,10 +37,10 @@ let abstract_tactic_expr ?(dflt=false) te tacfun gls = let abstract_tactic ?(dflt=false) te = !abstract_tactic_box := Some te; - abstract_tactic_expr ~dflt (Tacexpr.TacAtom (dummy_loc,te)) + abstract_tactic_expr ~dflt (Tacexpr.TacAtom (Loc.ghost,te)) let abstract_extended_tactic ?(dflt=false) s args = - abstract_tactic ~dflt (Tacexpr.TacExtend (dummy_loc, s, args)) + abstract_tactic ~dflt (Tacexpr.TacExtend (Loc.ghost, s, args)) let refiner = function | Prim pr -> diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli index 74c8314873..eca9ef807e 100644 --- a/proofs/tactic_debug.mli +++ b/proofs/tactic_debug.mli @@ -18,7 +18,7 @@ open Term Currently, it is quite simple and we can hope to have, in the future, a more complete panel of commands dedicated to a proof assistant framework *) -val set_tactic_printer : (glob_tactic_expr ->Pp.std_ppcmds) -> unit +val set_tactic_printer : (glob_tactic_expr -> Pp.std_ppcmds) -> unit val set_match_pattern_printer : (env -> constr_pattern match_pattern -> Pp.std_ppcmds) -> unit val set_match_rule_printer : @@ -78,4 +78,4 @@ val db_logic_failure : debug_info -> exn -> unit (** Prints a logic failure message for a rule *) val db_breakpoint : debug_info -> - identifier Pp.located message_token list -> unit + identifier Loc.located message_token list -> unit |