diff options
| -rw-r--r-- | interp/genarg.ml | 30 | ||||
| -rw-r--r-- | interp/genarg.mli | 6 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 1 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 1 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 1 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
6 files changed, 5 insertions, 36 deletions
diff --git a/interp/genarg.ml b/interp/genarg.ml index bbb4ae0a1..2daa1fe95 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -6,16 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp -open Errors -open Util open Names -open Nameops -open Nametab open Glob_term open Constrexpr -open Term -open Evd open Misctypes type argument_type = @@ -54,8 +47,6 @@ type open_glob_constr = unit * glob_constr_and_expr type glob_constr_pattern_and_expr = glob_constr_and_expr * Pattern.constr_pattern -type 'a with_ebindings = 'a * open_constr bindings - (* Dynamics but tagged by a type expression *) type 'a generic_argument = argument_type * Obj.t @@ -64,25 +55,6 @@ type rlevel type glevel type tlevel -let rec pr_intro_pattern (_,pat) = match pat with - | IntroOrAndPattern pll -> pr_or_and_intro_pattern pll - | IntroWildcard -> str "_" - | IntroRewrite true -> str "->" - | IntroRewrite false -> str "<-" - | IntroIdentifier id -> pr_id id - | IntroFresh id -> str "?" ++ pr_id id - | IntroForthcoming true -> str "*" - | IntroForthcoming false -> str "**" - | IntroAnonymous -> str "?" - -and pr_or_and_intro_pattern = function - | [pl] -> - str "(" ++ hv 0 (prlist_with_sep pr_comma pr_intro_pattern pl) ++ str ")" - | pll -> - str "[" ++ - hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll) - ++ str "]" - let rawwit_bool = BoolArgType let globwit_bool = BoolArgType let wit_bool = BoolArgType @@ -240,7 +212,7 @@ type ('a,'b) abstract_argument_type = argument_type let create_arg v s = if List.mem_assoc s !dyntab then - anomaly ("Genarg.create: already declared generic argument " ^ s); + Errors.anomaly ("Genarg.create: already declared generic argument " ^ s); let t = ExtraArgType s in dyntab := (s,Option.map (in_gen t) v) :: !dyntab; (t,t,t) diff --git a/interp/genarg.mli b/interp/genarg.mli index 7466ae46f..3986d135a 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors open Pp open Names open Term @@ -31,11 +30,6 @@ type open_glob_constr = unit * glob_constr_and_expr type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern -type 'a with_ebindings = 'a * open_constr bindings - -val pr_intro_pattern : intro_pattern_expr located -> Pp.std_ppcmds -val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds - (** The route of a generic argument, from parsing to evaluation. In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc. diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index bbfecac8f..6e9f475a3 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -21,6 +21,7 @@ open Ppextend open Ppconstr open Printer open Misctypes +open Miscops open Locus open Decl_kinds open Genredexpr diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 2047b5326..eb90c0549 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -18,6 +18,7 @@ open Pcoq open Tacticals open Constr open Misctypes +open Miscops let pr_binding prc = function | loc, NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 9b4df0ad5..462ffdc38 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -53,6 +53,7 @@ open Pcoq open Compat open Evd open Misctypes +open Miscops open Locus let safe_msgnl s = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ab4b08e7d..75f0b4a51 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -37,7 +37,6 @@ open Tacticals open Hipattern open Coqlib open Nametab -open Genarg open Tacexpr open Decl_kinds open Evarutil @@ -47,6 +46,7 @@ open Unification open Locus open Locusops open Misctypes +open Miscops exception Bound |