diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/decl_mode/decl_interp.ml | 5 | ||||
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 6 | ||||
| -rw-r--r-- | plugins/subtac/g_subtac.ml4 | 6 | ||||
| -rw-r--r-- | plugins/subtac/subtac.ml | 5 | ||||
| -rw-r--r-- | plugins/subtac/subtac_obligations.ml | 5 | ||||
| -rw-r--r-- | plugins/subtac/subtac_pretyping_F.ml | 5 |
6 files changed, 18 insertions, 14 deletions
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 1b91ef1776..aebe1fca45 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -17,6 +17,7 @@ open Pretyping.Default open Rawterm open Term open Pp +open Compat (* INTERN *) @@ -85,10 +86,10 @@ let intern_fundecl args body globs= let rec add_vars_of_simple_pattern globs = function CPatAlias (loc,p,id) -> add_vars_of_simple_pattern (add_var id globs) p -(* Stdpp.raise_with_loc loc +(* Loc.raise loc (UserError ("simple_pattern",str "\"as\" is not allowed here"))*) | CPatOr (loc, _)-> - Stdpp.raise_with_loc loc + Loc.raise loc (UserError ("simple_pattern",str "\"(_ | _)\" is not allowed here")) | CPatDelimiters (_,_,p) -> add_vars_of_simple_pattern globs p diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 28aa939750..11862747a3 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -11,7 +11,7 @@ (* arnaud: veiller à l'aspect tutorial des commentaires *) open Pp - +open Tok open Decl_expr open Names open Term @@ -85,9 +85,9 @@ let vernac_proof_instr instr = (* We create a new parser entry [proof_mode]. The Declarative proof mode will replace the normal parser entry for tactics with this one. *) -let proof_mode = Gram.Entry.create "vernac:proof_command" +let proof_mode = Gram.entry_create "vernac:proof_command" (* Auxiliary grammar entry. *) -let proof_instr = Gram.Entry.create "proofmode:instr" +let proof_instr = Gram.entry_create "proofmode:instr" (* Before we can write an new toplevel command (see below) which takes a [proof_instr] as argument, we need to declare diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4 index 9e415b635c..e186dd76dc 100644 --- a/plugins/subtac/g_subtac.ml4 +++ b/plugins/subtac/g_subtac.ml4 @@ -33,11 +33,11 @@ module Tactic = Pcoq.Tactic module SubtacGram = struct - let gec s = Gram.Entry.create ("Subtac."^s) + let gec s = Gram.entry_create ("Subtac."^s) (* types *) - let subtac_gallina_loc : Vernacexpr.vernac_expr located Gram.Entry.e = gec "subtac_gallina_loc" + let subtac_gallina_loc : Vernacexpr.vernac_expr located Gram.entry = gec "subtac_gallina_loc" - let subtac_withtac : Tacexpr.raw_tactic_expr option Gram.Entry.e = gec "subtac_withtac" + let subtac_withtac : Tacexpr.raw_tactic_expr option Gram.entry = gec "subtac_withtac" end open Rawterm diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml index 569aba2637..9214e451f4 100644 --- a/plugins/subtac/subtac.ml +++ b/plugins/subtac/subtac.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Compat open Global open Pp open Util @@ -228,8 +229,8 @@ let subtac (loc, command) = debug 2 (Himsg.explain_pretype_error env exn); raise e - | (Stdpp.Exc_located (loc, Proof_type.LtacLocated (_,e')) | - Stdpp.Exc_located (loc, e') as e) -> + | (Loc.Exc_located (loc, Proof_type.LtacLocated (_,e')) | + Loc.Exc_located (loc, e') as e) -> debug 2 (str "Parsing exception: "); (match e' with | Type_errors.TypeError (env, exn) -> diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index c7d0eb67fb..591e01c04e 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -15,6 +15,7 @@ open Util open Evd open Declare open Proof_type +open Compat let ppwarn cmd = Pp.warn (str"Program:" ++ cmd) let pperror cmd = Util.errorlabstrm "Program" cmd @@ -484,8 +485,8 @@ and solve_obligation_by_tac prg obls i tac = true else false with - | Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s))) - | Stdpp.Exc_located(_, Refiner.FailError (_, s)) + | Loc.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s))) + | Loc.Exc_located(_, Refiner.FailError (_, s)) | Refiner.FailError (_, s) -> user_err_loc (obl.obl_location, "solve_obligation", Lazy.force s) | Util.Anomaly _ as e -> raise e diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml index 0dda9b9e88..87c67cc147 100644 --- a/plugins/subtac/subtac_pretyping_F.ml +++ b/plugins/subtac/subtac_pretyping_F.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Compat open Util open Names open Sign @@ -270,7 +271,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | RCoFix i -> let cofix = (i,(names,ftys,fdefs)) in - (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e); + (try check_cofix env cofix with e -> Loc.raise loc e); make_judge (mkCoFix cofix) ftys.(i) in inh_conv_coerce_to_tycon loc env evdref fixj tycon @@ -357,7 +358,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let j' = pretype_type empty_valcon env' evdref lvar c2 in let resj = try judge_of_product env name j j' - with TypeError _ as e -> Stdpp.raise_with_loc loc e in + with TypeError _ as e -> Loc.raise loc e in inh_conv_coerce_to_tycon loc env evdref resj tycon | RLetIn(loc,name,c1,c2) -> |