diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml4 | 3 | ||||
| -rw-r--r-- | tactics/eauto.mli | 2 | ||||
| -rw-r--r-- | tactics/extraargs.mli | 14 | ||||
| -rw-r--r-- | tactics/rewrite.ml4 | 3 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 21 | ||||
| -rw-r--r-- | tactics/tactics.ml | 7 |
6 files changed, 27 insertions, 23 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 38ae4b9058..ba83fb5a80 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -35,6 +35,7 @@ open Pfedit open Command open Libnames open Evd +open Compat let default_eauto_depth = 100 let typeclasses_db = "typeclass_instances" @@ -205,7 +206,7 @@ let e_possible_resolve db_list local_db gl = let rec catchable = function | Refiner.FailError _ -> true - | Stdpp.Exc_located (_, e) -> catchable e + | Loc.Exc_located (_, e) -> catchable e | e -> Logic.catchable_exception e let is_ground gl = diff --git a/tactics/eauto.mli b/tactics/eauto.mli index 595917bdff..b51cb9d4be 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -15,7 +15,7 @@ open Evd open Environ open Explore -val hintbases : hint_db_name list option Pcoq.Gram.Entry.e +val hintbases : hint_db_name list option Pcoq.Gram.entry val wit_hintbases : hint_db_name list option typed_abstract_argument_type val rawwit_hintbases : hint_db_name list option raw_abstract_argument_type diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index ffa1bd747c..2c750be366 100644 --- a/tactics/extraargs.mli +++ b/tactics/extraargs.mli @@ -16,15 +16,15 @@ open Rawterm val rawwit_orient : bool raw_abstract_argument_type val wit_orient : bool typed_abstract_argument_type -val orient : bool Pcoq.Gram.Entry.e +val orient : bool Pcoq.Gram.entry -val occurrences : (int list or_var) Pcoq.Gram.Entry.e +val occurrences : (int list or_var) Pcoq.Gram.entry val rawwit_occurrences : (int list or_var) raw_abstract_argument_type val wit_occurrences : (int list) typed_abstract_argument_type val rawwit_raw : constr_expr raw_abstract_argument_type val wit_raw : (Tacinterp.interp_sign * rawconstr) typed_abstract_argument_type -val raw : constr_expr Pcoq.Gram.Entry.e +val raw : constr_expr Pcoq.Gram.entry type 'id gen_place= ('id * hyp_location_flag,unit) location @@ -33,17 +33,17 @@ type place = identifier gen_place val rawwit_hloc : loc_place raw_abstract_argument_type val wit_hloc : place typed_abstract_argument_type -val hloc : loc_place Pcoq.Gram.Entry.e +val hloc : loc_place Pcoq.Gram.entry -val in_arg_hyp: (Names.identifier Util.located list option * bool) Pcoq.Gram.Entry.e +val in_arg_hyp: (Names.identifier Util.located list option * bool) Pcoq.Gram.entry val rawwit_in_arg_hyp : (Names.identifier Util.located list option * bool) raw_abstract_argument_type val wit_in_arg_hyp : (Names.identifier list option * bool) typed_abstract_argument_type val raw_in_arg_hyp_to_clause : (Names.identifier Util.located list option * bool) -> Tacticals.clause val glob_in_arg_hyp_to_clause : (Names.identifier list option * bool) -> Tacticals.clause -val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.Entry.e +val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.entry val rawwit_by_arg_tac : raw_tactic_expr option raw_abstract_argument_type val wit_by_arg_tac : glob_tactic_expr option typed_abstract_argument_type @@ -51,6 +51,6 @@ val wit_by_arg_tac : glob_tactic_expr option typed_abstract_argument_type (** Spiwack: Primitive for retroknowledge registration *) -val retroknowledge_field : Retroknowledge.field Pcoq.Gram.Entry.e +val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry val rawwit_retroknowledge_field : Retroknowledge.field raw_abstract_argument_type val wit_retroknowledge_field : Retroknowledge.field typed_abstract_argument_type diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index d2381332ec..4827c77b63 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -36,6 +36,7 @@ open Pfedit open Command open Libnames open Evd +open Compat (** Typeclass-based generalized rewriting. *) @@ -1052,7 +1053,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl = else tclIDTAC in tclTHENLIST [evartac; rewtac] gl with - | Stdpp.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e))) + | Loc.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e))) | TypeClassError (env, (UnsatisfiableConstraints _ as e)) -> Refiner.tclFAIL_lazy 0 (lazy (str"setoid rewrite failed: unable to satisfy the rewriting constraints." diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 59d5cc3134..3d5f2ba1bb 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -46,6 +46,7 @@ open Pretyping open Pretyping.Default open Extrawit open Pcoq +open Compat let safe_msgnl s = try msgnl s with e -> @@ -90,15 +91,15 @@ let dloc = dummy_loc let catch_error call_trace tac g = if call_trace = [] then tac g else try tac g with | LtacLocated _ as e -> raise e - | Stdpp.Exc_located (_,LtacLocated _) as e -> raise e + | Loc.Exc_located (_,LtacLocated _) as e -> raise e | e -> let (nrep,loc',c),tail = list_sep_last call_trace in - let loc,e' = match e with Stdpp.Exc_located(loc,e) -> loc,e | _ ->dloc,e in + let loc,e' = match e with Loc.Exc_located(loc,e) -> loc,e | _ ->dloc,e in if tail = [] then let loc = if loc = dloc then loc' else loc in - raise (Stdpp.Exc_located(loc,e')) + raise (Loc.Exc_located(loc,e')) else - raise (Stdpp.Exc_located(loc',LtacLocated((nrep,c,tail,loc),e'))) + raise (Loc.Exc_located(loc',LtacLocated((nrep,c,tail,loc),e'))) (* Signature for interpretation: val_interp and interpretation functions *) type interp_sign = @@ -1955,14 +1956,14 @@ and eval_with_fail ist is_lazy goal tac = VRTactic (catch_error trace tac goal) | a -> a) with - | FailError (0,s) | Stdpp.Exc_located(_, FailError (0,s)) - | Stdpp.Exc_located(_,LtacLocated (_,FailError (0,s))) -> + | FailError (0,s) | Loc.Exc_located(_, FailError (0,s)) + | Loc.Exc_located(_,LtacLocated (_,FailError (0,s))) -> raise (Eval_fail (Lazy.force s)) | FailError (lvl,s) -> raise (FailError (lvl - 1, s)) - | Stdpp.Exc_located(s,FailError (lvl,s')) -> - raise (Stdpp.Exc_located(s,FailError (lvl - 1, s'))) - | Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) -> - raise (Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl - 1, s')))) + | Loc.Exc_located(s,FailError (lvl,s')) -> + raise (Loc.Exc_located(s,FailError (lvl - 1, s'))) + | Loc.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) -> + raise (Loc.Exc_located(s,LtacLocated (s'',FailError (lvl - 1, s')))) (* Interprets the clauses of a recursive LetIn *) and interp_letrec ist gl llc u = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 21a9ee258e..5c96c138ea 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Compat open Pp open Util open Names @@ -951,9 +952,9 @@ let general_apply with_delta with_destruct with_evars (loc,(c,lbind)) gl0 = with PretypeError _|RefinerError _|UserError _|Failure _|Exit -> if with_destruct then descend_in_conjunctions - try_main_apply (fun _ -> Stdpp.raise_with_loc loc exn) c gl + try_main_apply (fun _ -> Loc.raise loc exn) c gl else - Stdpp.raise_with_loc loc exn + Loc.raise loc exn in try_red_apply thm_ty0 in try_main_apply with_destruct c gl0 @@ -1109,7 +1110,7 @@ let clear_wildcards ids = try with_check (Tacmach.thin_no_check [id]) gl with ClearDependencyError (id,err) -> (* Intercept standard [thin] error message *) - Stdpp.raise_with_loc loc + Loc.raise loc (error_clear_dependency (pf_env gl) (id_of_string "_") err)) ids |