diff options
Diffstat (limited to 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/decl_interp.ml | 5 | ||||
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 6 |
2 files changed, 6 insertions, 5 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 |