From 2af78d3cca0f941841394b224b96f86903a68b10 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 21 May 2018 20:40:27 +0200 Subject: [api] Misctypes removal: multi to tactics/rewrite --- library/misctypes.ml | 6 ------ plugins/ltac/g_tactic.ml4 | 12 ++++++------ plugins/ltac/pptactic.ml | 2 +- plugins/ltac/tacexpr.ml | 2 +- plugins/ltac/tacexpr.mli | 2 +- tactics/equality.ml | 6 ++++++ tactics/equality.mli | 6 ++++++ 7 files changed, 21 insertions(+), 15 deletions(-) diff --git a/library/misctypes.ml b/library/misctypes.ml index cfae07484..ac8c7890c 100644 --- a/library/misctypes.ml +++ b/library/misctypes.ml @@ -106,9 +106,3 @@ type rec_flag = bool (* true = recursive false = not recursive *) type advanced_flag = bool (* true = advanced false = basic *) type letin_flag = bool (* true = use local def false = use Leibniz *) type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) - -type multi = - | Precisely of int - | UpTo of int - | RepeatStar - | RepeatPlus diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index dc9f607cf..15db4ca6a 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -494,12 +494,12 @@ GEXTEND Gram | -> None ] ] ; rewriter : - [ [ "!"; c = constr_with_bindings_arg -> (RepeatPlus,c) - | ["?"| LEFTQMARK]; c = constr_with_bindings_arg -> (RepeatStar,c) - | n = natural; "!"; c = constr_with_bindings_arg -> (Precisely n,c) - | n = natural; ["?" | LEFTQMARK]; c = constr_with_bindings_arg -> (UpTo n,c) - | n = natural; c = constr_with_bindings_arg -> (Precisely n,c) - | c = constr_with_bindings_arg -> (Precisely 1, c) + [ [ "!"; c = constr_with_bindings_arg -> (Equality.RepeatPlus,c) + | ["?"| LEFTQMARK]; c = constr_with_bindings_arg -> (Equality.RepeatStar,c) + | n = natural; "!"; c = constr_with_bindings_arg -> (Equality.Precisely n,c) + | n = natural; ["?" | LEFTQMARK]; c = constr_with_bindings_arg -> (Equality.UpTo n,c) + | n = natural; c = constr_with_bindings_arg -> (Equality.Precisely n,c) + | c = constr_with_bindings_arg -> (Equality.Precisely 1, c) ] ] ; oriented_rewriter : diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index b29af6680..894d91258 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -493,7 +493,7 @@ let string_of_genarg_arg (ArgumentType arg) = let pr_orient b = if b then mt () else str "<- " - let pr_multi = function + let pr_multi = let open Equality in function | Precisely 1 -> mt () | Precisely n -> int n ++ str "!" | UpTo n -> int n ++ str "?" diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 17f5e5d41..d6f7a461b 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -164,7 +164,7 @@ type 'a gen_atomic_tactic_expr = (* Equality and inversion *) | TacRewrite of evars_flag * - (bool * multi * 'dtrm with_bindings_arg) list * 'nam clause_expr * + (bool * Equality.multi * 'dtrm with_bindings_arg) list * 'nam clause_expr * (* spiwack: using ['dtrm] here is a small hack, may not be stable by a change in the representation of delayed terms. Because, in fact, it is the whole "with_bindings" diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 17f5e5d41..d6f7a461b 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -164,7 +164,7 @@ type 'a gen_atomic_tactic_expr = (* Equality and inversion *) | TacRewrite of evars_flag * - (bool * multi * 'dtrm with_bindings_arg) list * 'nam clause_expr * + (bool * Equality.multi * 'dtrm with_bindings_arg) list * 'nam clause_expr * (* spiwack: using ['dtrm] here is a small hack, may not be stable by a change in the representation of delayed terms. Because, in fact, it is the whole "with_bindings" diff --git a/tactics/equality.ml b/tactics/equality.ml index d7e697aed..c91758787 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -546,6 +546,12 @@ let apply_special_clear_request clear_flag f = e when catchable_exception e -> tclIDTAC end +type multi = + | Precisely of int + | UpTo of int + | RepeatStar + | RepeatPlus + let general_multi_rewrite with_evars l cl tac = let do1 l2r f = Proofview.Goal.enter begin fun gl -> diff --git a/tactics/equality.mli b/tactics/equality.mli index ccf454c3e..9395cf4a8 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -61,6 +61,12 @@ val general_rewrite_in : val general_rewrite_clause : orientation -> evars_flag -> ?tac:(unit Proofview.tactic * conditions) -> constr with_bindings -> clause -> unit Proofview.tactic +type multi = + | Precisely of int + | UpTo of int + | RepeatStar + | RepeatPlus + val general_multi_rewrite : evars_flag -> (bool * multi * clear_flag * delayed_open_constr_with_bindings) list -> clause -> (unit Proofview.tactic * conditions) option -> unit Proofview.tactic -- cgit v1.2.3 From 9367f1626afb080d10d425262dca705046a32933 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 21 May 2018 20:48:30 +0200 Subject: [api] Misctypes removal: module_kind to Declaremods --- interp/modintern.ml | 5 +++-- interp/modintern.mli | 3 +-- library/declaremods.ml | 6 ++++-- library/declaremods.mli | 8 ++++++-- library/misctypes.ml | 6 ------ 5 files changed, 14 insertions(+), 14 deletions(-) diff --git a/interp/modintern.ml b/interp/modintern.ml index fefd2ab6f..33c07d551 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -12,7 +12,7 @@ open Declarations open Libnames open Constrexpr open Constrintern -open Misctypes +open Declaremods type module_internalization_error = | NotAModuleNorModtype of string @@ -23,7 +23,7 @@ exception ModuleInternalizationError of module_internalization_error let error_not_a_module_loc kind loc qid = let s = string_of_qualid qid in - let e = match kind with + let e = let open Declaremods in match kind with | Module -> Modops.ModuleTypingError (Modops.NotAModule s) | ModType -> Modops.ModuleTypingError (Modops.NotAModuleType s) | ModAny -> ModuleInternalizationError (NotAModuleNorModtype s) @@ -46,6 +46,7 @@ let error_application_to_module_type loc = it is equal to the input kind when this one isn't ModAny. *) let lookup_module_or_modtype kind {CAst.loc;v=qid} = + let open Declaremods in try if kind == ModType then raise Not_found; let mp = Nametab.locate_module qid in diff --git a/interp/modintern.mli b/interp/modintern.mli index ef37aead8..529c438c1 100644 --- a/interp/modintern.mli +++ b/interp/modintern.mli @@ -11,7 +11,6 @@ open Environ open Entries open Constrexpr -open Misctypes (** Module internalization errors *) @@ -30,4 +29,4 @@ exception ModuleInternalizationError of module_internalization_error isn't ModAny. *) val interp_module_ast : - env -> module_kind -> module_ast -> module_struct_entry * module_kind * Univ.ContextSet.t + env -> Declaremods.module_kind -> module_ast -> module_struct_entry * Declaremods.module_kind * Univ.ContextSet.t diff --git a/library/declaremods.ml b/library/declaremods.ml index 1d5df49cf..e8d89f96b 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -36,6 +36,8 @@ type inline = | DefaultInline | InlineAt of int +type module_kind = Module | ModType | ModAny + let default_inline () = Some (Flags.get_inline_level ()) let inl2intopt = function @@ -994,8 +996,8 @@ let iter_all_segments f = (** {6 Some types used to shorten declaremods.mli} *) type 'modast module_interpretor = - Environ.env -> Misctypes.module_kind -> 'modast -> - Entries.module_struct_entry * Misctypes.module_kind * Univ.ContextSet.t + Environ.env -> module_kind -> 'modast -> + Entries.module_struct_entry * module_kind * Univ.ContextSet.t type 'modast module_params = (lident list * ('modast * inline)) list diff --git a/library/declaremods.mli b/library/declaremods.mli index 4aee7feae..63b25c7e4 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -27,9 +27,13 @@ type inline = | DefaultInline | InlineAt of int +(** Kinds of modules *) + +type module_kind = Module | ModType | ModAny + type 'modast module_interpretor = - Environ.env -> Misctypes.module_kind -> 'modast -> - Entries.module_struct_entry * Misctypes.module_kind * Univ.ContextSet.t + Environ.env -> module_kind -> 'modast -> + Entries.module_struct_entry * module_kind * Univ.ContextSet.t type 'modast module_params = (Misctypes.lident list * ('modast * inline)) list diff --git a/library/misctypes.ml b/library/misctypes.ml index ac8c7890c..a12caef80 100644 --- a/library/misctypes.ml +++ b/library/misctypes.ml @@ -75,7 +75,6 @@ type 'a bindings = type 'a with_bindings = 'a * 'a bindings - (** Some utility types for parsing *) type 'a or_var = @@ -93,11 +92,6 @@ type 'a or_by_notation = 'a or_by_notation_r CAst.t (* NB: the last string in [ByNotation] is actually a [Notation.delimiters], but this formulation avoids a useless dependency. *) - -(** Kinds of modules *) - -type module_kind = Module | ModType | ModAny - (** Various flags *) type direction_flag = bool (* true = Left-to-right false = right-to-right *) -- cgit v1.2.3 From 58630ad9a0b94a804a39a3d99f982965292692c7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 21 May 2018 23:54:55 +0200 Subject: [api] Misctypes removal: miscellaneous aliases. --- engine/evar_kinds.ml | 3 +-- engine/uState.ml | 2 +- engine/uState.mli | 4 ++-- engine/univNames.ml | 2 +- engine/univNames.mli | 2 +- interp/constrexpr.ml | 2 +- interp/constrintern.ml | 8 ++++---- interp/constrintern.mli | 1 - interp/declare.mli | 2 +- interp/dumpglob.mli | 4 ++-- interp/genredexpr.ml | 2 +- interp/implicit_quantifiers.ml | 2 +- interp/implicit_quantifiers.mli | 4 ++-- interp/reserve.mli | 2 +- kernel/names.ml | 6 ++++++ kernel/names.mli | 6 ++++++ library/declaremods.ml | 1 - library/declaremods.mli | 2 +- library/misctypes.ml | 12 ------------ plugins/ltac/g_tactic.ml4 | 9 +++++---- plugins/ltac/pltac.mli | 6 +++--- plugins/ltac/tactic_debug.mli | 2 +- pretyping/pattern.ml | 3 +++ pretyping/patternops.mli | 1 - pretyping/typeclasses.ml | 2 +- pretyping/typeclasses.mli | 2 +- pretyping/typeclasses_errors.ml | 2 +- pretyping/typeclasses_errors.mli | 4 ++-- printing/ppconstr.mli | 2 +- proofs/proof_global.ml | 2 +- proofs/proof_global.mli | 6 +++--- vernac/comFixpoint.ml | 1 - vernac/comFixpoint.mli | 2 +- vernac/egramcoq.ml | 2 +- vernac/indschemes.mli | 6 +++--- vernac/metasyntax.ml | 6 +++--- vernac/metasyntax.mli | 1 - vernac/obligations.ml | 4 ++-- vernac/obligations.mli | 4 ++-- 39 files changed, 66 insertions(+), 68 deletions(-) diff --git a/engine/evar_kinds.ml b/engine/evar_kinds.ml index 6e123d642..12e2fda8e 100644 --- a/engine/evar_kinds.ml +++ b/engine/evar_kinds.ml @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Misctypes (** The kinds of existential variable *) @@ -18,7 +17,7 @@ open Misctypes type obligation_definition_status = Define of bool | Expand -type matching_var_kind = FirstOrderPatVar of patvar | SecondOrderPatVar of patvar +type matching_var_kind = FirstOrderPatVar of Id.t | SecondOrderPatVar of Id.t type subevar_kind = Domain | Codomain | Body diff --git a/engine/uState.ml b/engine/uState.ml index 643c621fd..0e3ecdbf5 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -312,7 +312,7 @@ type ('a, 'b) gen_universe_decl = { univdecl_extensible_constraints : bool (* Can new constraints be added *) } type universe_decl = - (Misctypes.lident list, Univ.Constraint.t) gen_universe_decl + (lident list, Univ.Constraint.t) gen_universe_decl let default_univ_decl = { univdecl_instance = []; diff --git a/engine/uState.mli b/engine/uState.mli index e2f25642e..e7e5b39e0 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -26,7 +26,7 @@ val empty : t val make : UGraph.t -> t -val make_with_initial_binders : UGraph.t -> Misctypes.lident list -> t +val make_with_initial_binders : UGraph.t -> lident list -> t val is_empty : t -> bool @@ -145,7 +145,7 @@ type ('a, 'b) gen_universe_decl = { univdecl_extensible_constraints : bool (* Can new constraints be added *) } type universe_decl = - (Misctypes.lident list, Univ.Constraint.t) gen_universe_decl + (lident list, Univ.Constraint.t) gen_universe_decl val default_univ_decl : universe_decl diff --git a/engine/univNames.ml b/engine/univNames.ml index 6e59a7c9e..6ffb4bcf0 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -89,7 +89,7 @@ let register_universe_binders ref ubinders = if not (Id.Map.is_empty ubinders) then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders)) -type univ_name_list = Misctypes.lname list +type univ_name_list = Names.lname list let universe_binders_with_opt_names ref levels = function | None -> universe_binders_of_global ref diff --git a/engine/univNames.mli b/engine/univNames.mli index e3bc3193d..c19aa19d5 100644 --- a/engine/univNames.mli +++ b/engine/univNames.mli @@ -29,7 +29,7 @@ val empty_binders : universe_binders val register_universe_binders : Names.GlobRef.t -> universe_binders -> unit val universe_binders_of_global : Names.GlobRef.t -> universe_binders -type univ_name_list = Misctypes.lname list +type univ_name_list = Names.lname list (** [universe_binders_with_opt_names ref u l] diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index ca6ea94f0..d6b395e01 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -95,7 +95,7 @@ and constr_expr_r = | CIf of constr_expr * (lname option * constr_expr option) * constr_expr * constr_expr | CHole of Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option - | CPatVar of patvar + | CPatVar of Pattern.patvar | CEvar of Glob_term.existential_name * (Id.t * constr_expr) list | CSort of Glob_term.glob_sort | CCast of constr_expr * constr_expr cast_type diff --git a/interp/constrintern.ml b/interp/constrintern.ml index e09b7a793..057e10c00 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -606,7 +606,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam (renaming',env), None, Name id' type binder_action = -| AddLetIn of Misctypes.lname * constr_expr * constr_expr option +| AddLetIn of lname * constr_expr * constr_expr option | AddTermIter of (constr_expr * subscopes) Names.Id.Map.t | AddPreBinderIter of Id.t * local_binder_expr (* A binder to be internalized *) | AddBinderIter of Id.t * extended_glob_local_binder (* A binder already internalized - used for generalized binders *) @@ -1073,11 +1073,11 @@ let interp_reference vars r = (** Private internalization patterns *) type 'a raw_cases_pattern_expr_r = - | RCPatAlias of 'a raw_cases_pattern_expr * Misctypes.lname + | RCPatAlias of 'a raw_cases_pattern_expr * lname | RCPatCstr of GlobRef.t * 'a raw_cases_pattern_expr list * 'a raw_cases_pattern_expr list (** [RCPatCstr (loc, c, l1, l2)] represents [((@ c l1) l2)] *) - | RCPatAtom of (Misctypes.lident * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option + | RCPatAtom of (lident * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option | RCPatOr of 'a raw_cases_pattern_expr list and 'a raw_cases_pattern_expr = ('a raw_cases_pattern_expr_r, 'a) DAst.t @@ -1385,7 +1385,7 @@ let sort_fields ~complete loc fields completer = (** {6 Manage multiple aliases} *) type alias = { - alias_ids : Misctypes.lident list; + alias_ids : lident list; alias_map : Id.t Id.Map.t; } diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 4dd719e1f..12f77af30 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -11,7 +11,6 @@ open Names open Evd open Environ -open Misctypes open Libnames open Glob_term open Pattern diff --git a/interp/declare.mli b/interp/declare.mli index 4a9f54278..02e73cd66 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -87,6 +87,6 @@ val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit -val do_universe : polymorphic -> Misctypes.lident list -> unit +val do_universe : polymorphic -> lident list -> unit val do_constraint : polymorphic -> (Glob_term.glob_level * Univ.constraint_type * Glob_term.glob_level) list -> unit diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index bf83d2df4..931d05a97 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -27,7 +27,7 @@ val continue : unit -> unit val add_glob : ?loc:Loc.t -> Names.GlobRef.t -> unit val add_glob_kn : ?loc:Loc.t -> Names.KerName.t -> unit -val dump_definition : Misctypes.lident -> bool -> string -> unit +val dump_definition : Names.lident -> bool -> string -> unit val dump_moddef : ?loc:Loc.t -> Names.ModPath.t -> string -> unit val dump_modref : ?loc:Loc.t -> Names.ModPath.t -> string -> unit val dump_reference : ?loc:Loc.t -> string -> string -> string -> unit @@ -39,7 +39,7 @@ val dump_notation : (Constrexpr.notation * Notation.notation_location) Loc.located -> Notation_term.scope_name option -> bool -> unit -val dump_constraint : Misctypes.lname -> bool -> string -> unit +val dump_constraint : Names.lname -> bool -> string -> unit val dump_string : string -> unit diff --git a/interp/genredexpr.ml b/interp/genredexpr.ml index 80697461a..983493b25 100644 --- a/interp/genredexpr.ml +++ b/interp/genredexpr.ml @@ -52,7 +52,7 @@ type ('a,'b,'c) red_expr_gen = type ('a,'b,'c) may_eval = | ConstrTerm of 'a | ConstrEval of ('a,'b,'c) red_expr_gen * 'a - | ConstrContext of Misctypes.lident * 'a + | ConstrContext of Names.lident * 'a | ConstrTypeOf of 'a open Libnames diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index b48db9ac5..b54e2badd 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -53,7 +53,7 @@ let cache_generalizable_type (_,(local,cmd)) = let load_generalizable_type _ (_,(local,cmd)) = generalizable_table := add_generalizable cmd !generalizable_table -let in_generalizable : bool * Misctypes.lident list option -> obj = +let in_generalizable : bool * lident list option -> obj = declare_object {(default_object "GENERALIZED-IDENT") with load_function = load_generalizable_type; cache_function = cache_generalizable_type; diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index e64c5c542..25394fc0d 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -13,7 +13,7 @@ open Glob_term open Constrexpr open Libnames -val declare_generalizable : local:bool -> Misctypes.lident list option -> unit +val declare_generalizable : local:bool -> lident list option -> unit val ids_of_list : Id.t list -> Id.Set.t val destClassApp : constr_expr -> (reference * constr_expr list * instance_expr option) CAst.t @@ -31,7 +31,7 @@ val free_vars_of_binders : order with the location of their first occurrence *) val generalizable_vars_of_glob_constr : ?bound:Id.Set.t -> ?allowed:Id.Set.t -> - glob_constr -> Misctypes.lident list + glob_constr -> lident list val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t diff --git a/interp/reserve.mli b/interp/reserve.mli index daee58639..a10858e71 100644 --- a/interp/reserve.mli +++ b/interp/reserve.mli @@ -11,5 +11,5 @@ open Names open Notation_term -val declare_reserved_type : Misctypes.lident list -> notation_constr -> unit +val declare_reserved_type : lident list -> notation_constr -> unit val find_reserved_type : Id.t -> notation_constr diff --git a/kernel/names.ml b/kernel/names.ml index 54f089e60..597061278 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -852,3 +852,9 @@ let eq_egr e1 e2 = match e1, e2 with EvalConstRef con1, EvalConstRef con2 -> Constant.equal con1 con2 | EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2 | _, _ -> false + +(** Located identifiers and objects with syntax. *) + +type lident = Id.t CAst.t +type lname = Name.t CAst.t +type lstring = string CAst.t diff --git a/kernel/names.mli b/kernel/names.mli index f988b559a..4eb5adb62 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -605,3 +605,9 @@ type evaluable_global_reference = | EvalConstRef of Constant.t val eq_egr : evaluable_global_reference -> evaluable_global_reference -> bool + +(** Located identifiers and objects with syntax. *) + +type lident = Id.t CAst.t +type lname = Name.t CAst.t +type lstring = string CAst.t diff --git a/library/declaremods.ml b/library/declaremods.ml index e8d89f96b..0b3b461e6 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -17,7 +17,6 @@ open Entries open Libnames open Libobject open Mod_subst -open Misctypes (** {6 Inlining levels} *) diff --git a/library/declaremods.mli b/library/declaremods.mli index 63b25c7e4..b42a59bfb 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -36,7 +36,7 @@ type 'modast module_interpretor = Entries.module_struct_entry * module_kind * Univ.ContextSet.t type 'modast module_params = - (Misctypes.lident list * ('modast * inline)) list + (lident list * ('modast * inline)) list (** [declare_module interp_modast id fargs typ exprs] declares module [id], with structure constructed by [interp_modast] diff --git a/library/misctypes.ml b/library/misctypes.ml index a12caef80..3b629f449 100644 --- a/library/misctypes.ml +++ b/library/misctypes.ml @@ -10,18 +10,6 @@ open Names -(** Basic types used both in [constr_expr], [glob_constr], and [vernacexpr] *) - -(** Located identifiers and objects with syntax. *) - -type lident = Id.t CAst.t -type lname = Name.t CAst.t -type lstring = string CAst.t - -(** Cases pattern variables *) - -type patvar = Id.t - (** Introduction patterns *) type 'constr intro_pattern_expr = diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 15db4ca6a..038d55e4b 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -11,6 +11,7 @@ open Pp open CErrors open Util +open Names open Tacexpr open Genredexpr open Constrexpr @@ -383,19 +384,19 @@ GEXTEND Gram ; hypident: [ [ id = id_or_meta -> - let id : Misctypes.lident = id in + let id : lident = id in id,InHyp | "("; IDENT "type"; IDENT "of"; id = id_or_meta; ")" -> - let id : Misctypes.lident = id in + let id : lident = id in id,InHypTypeOnly | "("; IDENT "value"; IDENT "of"; id = id_or_meta; ")" -> - let id : Misctypes.lident = id in + let id : lident = id in id,InHypValueOnly ] ] ; hypident_occ: [ [ (id,l)=hypident; occs=occs -> - let id : Misctypes.lident = id in + let id : lident = id in ((occs,id),l) ] ] ; in_clause: diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index 434feba95..de23d2f8e 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -20,7 +20,7 @@ open Misctypes val open_constr : constr_expr Gram.entry val constr_with_bindings : constr_expr with_bindings Gram.entry val bindings : constr_expr bindings Gram.entry -val hypident : (lident * Locus.hyp_location_flag) Gram.entry +val hypident : (Names.lident * Locus.hyp_location_flag) Gram.entry val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry val uconstr : constr_expr Gram.entry @@ -29,8 +29,8 @@ val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Gram.ent val int_or_var : int or_var Gram.entry val simple_tactic : raw_tactic_expr Gram.entry val simple_intropattern : constr_expr intro_pattern_expr CAst.t Gram.entry -val in_clause : lident Locus.clause_expr Gram.entry -val clause_dft_concl : lident Locus.clause_expr Gram.entry +val in_clause : Names.lident Locus.clause_expr Gram.entry +val clause_dft_concl : Names.lident Locus.clause_expr Gram.entry val tactic_arg : raw_tactic_arg Gram.entry val tactic_expr : raw_tactic_expr Gram.entry val binder_tactic : raw_tactic_expr Gram.entry diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli index 734e76b56..175341df0 100644 --- a/plugins/ltac/tactic_debug.mli +++ b/plugins/ltac/tactic_debug.mli @@ -76,7 +76,7 @@ val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t (** Prints a logic failure message for a rule *) val db_breakpoint : debug_info -> - Misctypes.lident message_token list -> unit Proofview.NonLogical.t + lident message_token list -> unit Proofview.NonLogical.t val extract_ltac_trace : ?loc:Loc.t -> Tacexpr.ltac_trace -> Pp.t option Loc.located diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 996a2dc36..519a5466b 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -13,6 +13,9 @@ open Misctypes (** {5 Patterns} *) +(** Cases pattern variables *) +type patvar = Id.t + type case_info_pattern = { cip_style : Constr.case_style; cip_ind : inductive option; diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index dfbfb147f..36317b3ac 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -10,7 +10,6 @@ open Names open Mod_subst -open Misctypes open Glob_term open Pattern open EConstr diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 70588b6ad..d3aa7ac64 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -30,7 +30,7 @@ type 'a hint_info_gen = { hint_priority : int option; hint_pattern : 'a option } -type hint_info = (Misctypes.patvar list * Pattern.constr_pattern) hint_info_gen +type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen let typeclasses_unique_solutions = ref false let set_typeclasses_unique_solutions d = (:=) typeclasses_unique_solutions d diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index c78382c82..e4a56960c 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -21,7 +21,7 @@ type 'a hint_info_gen = { hint_priority : int option; hint_pattern : 'a option } -type hint_info = (Misctypes.patvar list * Pattern.constr_pattern) hint_info_gen +type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen (** This module defines type-classes *) type typeclass = { diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index a1ac53c73..2720a3e4d 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -18,7 +18,7 @@ type contexts = Parameters | Properties type typeclass_error = | NotAClass of constr - | UnboundMethod of GlobRef.t * Misctypes.lident (* Class name, method *) + | UnboundMethod of GlobRef.t * lident (* Class name, method *) exception TypeClassError of env * typeclass_error diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index 1003f2ae1..9831627a9 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -16,11 +16,11 @@ type contexts = Parameters | Properties type typeclass_error = | NotAClass of constr - | UnboundMethod of GlobRef.t * Misctypes.lident (** Class name, method *) + | UnboundMethod of GlobRef.t * lident (** Class name, method *) exception TypeClassError of env * typeclass_error val not_a_class : env -> constr -> 'a -val unbound_method : env -> GlobRef.t -> Misctypes.lident -> 'a +val unbound_method : env -> GlobRef.t -> lident -> 'a diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 05f48ec79..89df8f5b9 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -39,7 +39,7 @@ val pr_name : Name.t -> Pp.t [@@ocaml.deprecated "alias of Names.Name.print"] val pr_qualid : qualid -> Pp.t -val pr_patvar : patvar -> Pp.t +val pr_patvar : Pattern.patvar -> Pp.t val pr_glob_level : Glob_term.glob_level -> Pp.t val pr_glob_sort : Glob_term.glob_sort -> Pp.t diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 946379356..3120c97b5 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -83,7 +83,7 @@ type opacity_flag = Opaque | Transparent type proof_ending = | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t | Proved of opacity_flag * - Misctypes.lident option * + lident option * proof_object type proof_terminator = proof_ending -> unit diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 0141cacb9..9e07ed2d0 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -22,7 +22,7 @@ val check_no_pending_proof : unit -> unit val get_current_proof_name : unit -> Names.Id.t val get_all_proof_names : unit -> Names.Id.t list -val discard : Misctypes.lident -> unit +val discard : Names.lident -> unit val discard_current : unit -> unit val discard_all : unit -> unit @@ -54,7 +54,7 @@ type proof_ending = | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t | Proved of opacity_flag * - Misctypes.lident option * + Names.lident option * proof_object type proof_terminator type closed_proof = proof_object * proof_terminator @@ -126,7 +126,7 @@ val set_endline_tactic : Genarg.glob_generic_argument -> unit * (w.r.t. type dependencies and let-ins covered by it) + a list of * ids to be cleared *) val set_used_variables : - Names.Id.t list -> Context.Named.t * Misctypes.lident list + Names.Id.t list -> Context.Named.t * Names.lident list val get_used_variables : unit -> Context.Named.t option (** Get the universe declaration associated to the current proof. *) diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index b5b8697d2..1d1cc62de 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -13,7 +13,6 @@ open Decl_kinds open Pretyping open Evarutil open Evarconv -open Misctypes module RelDecl = Context.Rel.Declaration diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index a6992a30b..f51bfbad5 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -33,7 +33,7 @@ val do_cofixpoint : type structured_fixpoint_expr = { fix_name : Id.t; fix_univs : Constrexpr.universe_decl_expr option; - fix_annot : Misctypes.lident option; + fix_annot : lident option; fix_binders : local_binder_expr list; fix_body : constr_expr option; fix_type : constr_expr diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index e7a308dda..434e836d8 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -228,7 +228,7 @@ type _ target = type prod_info = production_level * production_position type (_, _) entry = -| TTName : ('self, Misctypes.lname) entry +| TTName : ('self, lname) entry | TTReference : ('self, reference) entry | TTBigint : ('self, Constrexpr.raw_natural_number) entry | TTConstr : prod_info * 'r target -> ('r, 'r) entry diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli index bd4249cac..261c3d813 100644 --- a/vernac/indschemes.mli +++ b/vernac/indschemes.mli @@ -32,17 +32,17 @@ val declare_rewriting_schemes : inductive -> unit (** Mutual Minimality/Induction scheme *) val do_mutual_induction_scheme : - (Misctypes.lident * bool * inductive * Sorts.family) list -> unit + (lident * bool * inductive * Sorts.family) list -> unit (** Main calls to interpret the Scheme command *) -val do_scheme : (Misctypes.lident option * scheme) list -> unit +val do_scheme : (lident option * scheme) list -> unit (** Combine a list of schemes into a conjunction of them *) val build_combined_scheme : env -> Constant.t list -> Evd.evar_map * constr * types -val do_combined_scheme : Misctypes.lident -> Misctypes.lident list -> unit +val do_combined_scheme : lident -> lident list -> unit (** Hook called at each inductive type definition *) diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 2245e762f..8f64f5519 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -92,7 +92,7 @@ let pr_grammar = function (* Parse a format (every terminal starting with a letter or a single quote (except a single quote alone) must be quoted) *) -let parse_format ({CAst.loc;v=str} : Misctypes.lstring) = +let parse_format ({CAst.loc;v=str} : lstring) = let len = String.length str in (* TODO: update the line of the location when the string contains newlines *) let make_loc i j = Option.map (Loc.shift_loc (i+1) (j-len)) loc in @@ -792,7 +792,7 @@ type notation_modifier = { only_parsing : bool; only_printing : bool; compat : Flags.compat_version option; - format : Misctypes.lstring option; + format : lstring option; extra : (string * string) list; } @@ -1104,7 +1104,7 @@ module SynData = struct only_parsing : bool; only_printing : bool; compat : Flags.compat_version option; - format : Misctypes.lstring option; + format : lstring option; extra : (string * string) list; (* XXX: Callback to printing, must remove *) diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli index a6c12e089..f6de75b07 100644 --- a/vernac/metasyntax.mli +++ b/vernac/metasyntax.mli @@ -14,7 +14,6 @@ open Notation open Constrexpr open Notation_term open Environ -open Misctypes val add_token_obj : string -> unit diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 00f1760c2..1ab24b670 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -298,10 +298,10 @@ type obligation = type obligations = (obligation array * int) type fixpoint_kind = - | IsFixpoint of (Misctypes.lident option * Constrexpr.recursion_order_expr) list + | IsFixpoint of (lident option * Constrexpr.recursion_order_expr) list | IsCoFixpoint -type notations = (Misctypes.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list +type notations = (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list type program_info_aux = { prg_name: Id.t; diff --git a/vernac/obligations.mli b/vernac/obligations.mli index b1eaf51ac..a37c30aaf 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -62,10 +62,10 @@ val add_definition : Names.Id.t -> ?term:constr -> types -> ?hook:(UState.t -> unit) Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress type notations = - (Misctypes.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list + (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list type fixpoint_kind = - | IsFixpoint of (Misctypes.lident option * Constrexpr.recursion_order_expr) list + | IsFixpoint of (lident option * Constrexpr.recursion_order_expr) list | IsCoFixpoint val add_mutual_definitions : -- cgit v1.2.3 From 36a98d55576ebdb106a55c3bd682961da8d77dee Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 21 May 2018 23:57:32 +0200 Subject: [api] Misctypes removal: remove dummy alias. --- library/misctypes.ml | 4 ---- pretyping/pattern.ml | 3 +-- 2 files changed, 1 insertion(+), 6 deletions(-) diff --git a/library/misctypes.ml b/library/misctypes.ml index 3b629f449..7cd1a83be 100644 --- a/library/misctypes.ml +++ b/library/misctypes.ml @@ -38,10 +38,6 @@ type 'id move_location = | MoveFirst | MoveLast (** can be seen as "no move" when doing intro *) -(** A synonym of [Evar.t], also defined in Term *) - -type existential_key = Evar.t - (** Casts *) type 'a cast_type = diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 519a5466b..be7ebe49c 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Misctypes (** {5 Patterns} *) @@ -25,7 +24,7 @@ type case_info_pattern = type constr_pattern = | PRef of GlobRef.t | PVar of Id.t - | PEvar of existential_key * constr_pattern array + | PEvar of Evar.t * constr_pattern array | PRel of int | PApp of constr_pattern * constr_pattern array | PSoApp of patvar * constr_pattern list -- cgit v1.2.3 From 368a25e4ef14512b00f5799e26c3f615bc540201 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 22 May 2018 00:07:26 +0200 Subject: [api] Misctypes removal: several moves: - move_location to proofs/logic. - intro_pattern_naming to Namegen. --- dev/base_include | 2 - engine/evarutil.ml | 8 +-- engine/evarutil.mli | 15 +++--- engine/namegen.ml | 12 +++++ engine/namegen.mli | 10 ++++ interp/constrexpr.ml | 5 +- interp/constrexpr_ops.ml | 11 +++-- interp/constrexpr_ops.mli | 3 +- interp/constrextern.ml | 13 ++--- interp/constrintern.ml | 34 ++++++------- interp/notation_ops.ml | 22 ++++----- interp/notation_term.ml | 3 +- interp/tactypes.ml | 32 +++++++++++- library/misctypes.ml | 86 --------------------------------- parsing/g_constr.ml4 | 2 +- plugins/cc/cctac.ml | 2 +- plugins/firstorder/instances.ml | 5 +- plugins/funind/g_indfun.ml4 | 2 +- plugins/funind/glob_term_to_relation.ml | 1 - plugins/funind/glob_termops.ml | 11 ++--- plugins/funind/indfun.ml | 4 +- plugins/funind/indfun.mli | 2 +- plugins/funind/invfun.ml | 6 +-- plugins/funind/invfun.mli | 2 +- plugins/funind/recdef.ml | 2 +- plugins/ltac/coretactics.ml4 | 2 + plugins/ltac/evar_tactics.ml | 2 +- plugins/ltac/extratactics.ml4 | 9 ++-- plugins/ltac/g_ltac.ml4 | 2 + plugins/ltac/g_rewrite.ml4 | 2 +- plugins/ltac/g_tactic.ml4 | 2 + plugins/ltac/pltac.mli | 1 + plugins/ltac/pptactic.ml | 3 +- plugins/ltac/pptactic.mli | 1 + plugins/ltac/rewrite.ml | 4 +- plugins/ltac/rewrite.mli | 4 +- plugins/ltac/tacarg.mli | 2 +- plugins/ltac/taccoerce.ml | 2 + plugins/ltac/taccoerce.mli | 3 +- plugins/ltac/tacexpr.ml | 7 +-- plugins/ltac/tacexpr.mli | 7 +-- plugins/ltac/tacintern.ml | 2 + plugins/ltac/tacintern.mli | 2 +- plugins/ltac/tacinterp.ml | 2 + plugins/ltac/tacinterp.mli | 1 + plugins/ltac/tacsubst.ml | 1 + plugins/ltac/tacsubst.mli | 2 +- plugins/ltac/tauto.ml | 4 +- plugins/micromega/coq_micromega.ml | 5 +- plugins/omega/coq_omega.ml | 2 +- plugins/ssr/ssrcommon.ml | 8 +-- plugins/ssr/ssrelim.ml | 2 +- plugins/ssr/ssrfwd.ml | 1 - plugins/ssr/ssrparser.ml4 | 18 +++---- plugins/ssr/ssrview.ml | 2 +- plugins/ssrmatching/ssrmatching.ml4 | 2 +- pretyping/cases.ml | 2 +- pretyping/detyping.ml | 3 +- pretyping/glob_ops.ml | 35 +++++++++++--- pretyping/glob_ops.mli | 9 +++- pretyping/glob_term.ml | 11 ++++- pretyping/miscops.ml | 55 --------------------- pretyping/miscops.mli | 30 ------------ pretyping/misctypes.ml | 37 ++++++++++++++ pretyping/patternops.ml | 5 +- pretyping/pretyping.ml | 1 - printing/ppconstr.ml | 17 ++++--- proofs/clenv.ml | 2 +- proofs/clenv.mli | 2 +- proofs/logic.ml | 19 +++++++- proofs/logic.mli | 15 +++++- proofs/miscprint.ml | 12 +---- proofs/miscprint.mli | 7 +-- tactics/contradiction.ml | 3 +- tactics/contradiction.mli | 2 +- tactics/eqdecide.ml | 10 ++-- tactics/equality.ml | 1 + tactics/hipattern.ml | 2 +- tactics/inv.ml | 14 +++--- tactics/inv.mli | 1 - tactics/leminv.mli | 2 +- tactics/tacticals.ml | 4 +- tactics/tactics.ml | 1 + tactics/tactics.mli | 12 ++--- vernac/auto_ind_decl.ml | 3 +- vernac/classes.ml | 4 +- vernac/g_proofs.ml4 | 2 +- vernac/g_vernac.ml4 | 8 +-- vernac/ppvernac.ml | 2 +- vernac/record.ml | 2 +- 90 files changed, 359 insertions(+), 378 deletions(-) delete mode 100644 library/misctypes.ml delete mode 100644 pretyping/miscops.ml delete mode 100644 pretyping/miscops.mli create mode 100644 pretyping/misctypes.ml diff --git a/dev/base_include b/dev/base_include index fc38305cc..574bc097e 100644 --- a/dev/base_include +++ b/dev/base_include @@ -108,8 +108,6 @@ open Inductiveops open Locusops open Find_subterm open Unification -open Miscops -open Miscops open Nativenorm open Typeclasses open Typeclasses_errors diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 648f96035..82be4791f 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -436,12 +436,12 @@ let new_pure_evar_full evd evi = (evd, evk) let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) sign evd typ = - let default_naming = Misctypes.IntroAnonymous in + let default_naming = IntroAnonymous in let naming = Option.default default_naming naming in let name = match naming with - | Misctypes.IntroAnonymous -> None - | Misctypes.IntroIdentifier id -> Some id - | Misctypes.IntroFresh id -> + | IntroAnonymous -> None + | IntroIdentifier id -> Some id + | IntroFresh id -> let has_name id = try let _ = Evd.evar_key id evd in true with Not_found -> false in let id = Namegen.next_ident_away_from id has_name in Some id diff --git a/engine/evarutil.mli b/engine/evarutil.mli index f83f262b4..c17f3d168 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -12,6 +12,7 @@ open Names open Constr open Evd open Environ +open Namegen open EConstr (** This module provides useful higher-level functions for evar manipulation. *) @@ -27,7 +28,7 @@ val mk_new_meta : unit -> constr val new_evar_from_context : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> + ?naming:intro_pattern_naming_expr -> ?principal:bool -> named_context_val -> evar_map -> types -> evar_map * EConstr.t @@ -40,14 +41,14 @@ type naming_mode = val new_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> + ?naming:intro_pattern_naming_expr -> ?principal:bool -> ?hypnaming:naming_mode -> env -> evar_map -> types -> evar_map * EConstr.t val new_pure_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> + ?naming:intro_pattern_naming_expr -> ?principal:bool -> named_context_val -> evar_map -> types -> evar_map * Evar.t @@ -57,7 +58,7 @@ val new_pure_evar_full : evar_map -> evar_info -> evar_map * Evar.t them during type-checking and unification. *) val new_type_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> + ?naming:intro_pattern_naming_expr -> ?principal:bool -> ?hypnaming:naming_mode -> env -> evar_map -> rigid -> evar_map * (constr * Sorts.t) @@ -79,7 +80,7 @@ val new_global : evar_map -> GlobRef.t -> evar_map * constr as a telescope) is [sign] *) val new_evar_instance : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> - ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> + ?store:Store.t -> ?naming:intro_pattern_naming_expr -> ?principal:bool -> named_context_val -> evar_map -> types -> constr list -> evar_map * constr @@ -262,13 +263,13 @@ val meta_counter_summary_tag : int Summary.Dyn.tag val e_new_evar : env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> + ?naming:intro_pattern_naming_expr -> ?principal:bool -> ?hypnaming:naming_mode -> types -> constr [@@ocaml.deprecated "Use [Evarutil.new_evar]"] val e_new_type_evar : env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> + ?naming:intro_pattern_naming_expr -> ?principal:bool -> ?hypnaming:naming_mode -> rigid -> constr * Sorts.t [@@ocaml.deprecated "Use [Evarutil.new_type_evar]"] diff --git a/engine/namegen.ml b/engine/namegen.ml index c069ec5a0..23c691139 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -29,6 +29,18 @@ open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration +(** General evar naming using intro patterns *) +type intro_pattern_naming_expr = + | IntroIdentifier of Id.t + | IntroFresh of Id.t + | IntroAnonymous + +let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with +| IntroAnonymous, IntroAnonymous -> true +| IntroIdentifier id1, IntroIdentifier id2 -> Names.Id.equal id1 id2 +| IntroFresh id1, IntroFresh id2 -> Names.Id.equal id1 id2 +| _ -> false + (**********************************************************************) (* Conventional names *) diff --git a/engine/namegen.mli b/engine/namegen.mli index 1b70ef68d..a53c3a0d1 100644 --- a/engine/namegen.mli +++ b/engine/namegen.mli @@ -15,6 +15,16 @@ open Environ open Evd open EConstr +(** General evar naming using intro patterns *) +type intro_pattern_naming_expr = + | IntroIdentifier of Id.t + | IntroFresh of Id.t + | IntroAnonymous + +(** Equalities on [intro_pattern_naming] *) +val intro_pattern_naming_eq : + intro_pattern_naming_expr -> intro_pattern_naming_expr -> bool + (********************************************************************* Conventional default names *) diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index d6b395e01..60f2c683a 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -10,7 +10,6 @@ open Names open Libnames -open Misctypes open Decl_kinds (** {6 Concrete syntax for terms } *) @@ -94,11 +93,11 @@ and constr_expr_r = constr_expr * constr_expr | CIf of constr_expr * (lname option * constr_expr option) * constr_expr * constr_expr - | CHole of Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option + | CHole of Evar_kinds.t option * Namegen.intro_pattern_naming_expr * Genarg.raw_generic_argument option | CPatVar of Pattern.patvar | CEvar of Glob_term.existential_name * (Id.t * constr_expr) list | CSort of Glob_term.glob_sort - | CCast of constr_expr * constr_expr cast_type + | CCast of constr_expr * constr_expr Glob_term.cast_type | CNotation of notation * constr_notation_substitution | CGeneralization of binding_kind * abstraction_kind option * constr_expr | CPrim of prim_token diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 1be1dd96c..d626630ef 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -14,8 +14,9 @@ open CAst open Names open Nameops open Libnames +open Namegen +open Glob_term open Constrexpr -open Misctypes open Decl_kinds (***********************) @@ -161,7 +162,7 @@ let rec constr_expr_eq e1 e2 = | CEvar (id1, c1), CEvar (id2, c2) -> Id.equal id1 id2 && List.equal instance_eq c1 c2 | CSort s1, CSort s2 -> - Miscops.glob_sort_eq s1 s2 + Glob_ops.glob_sort_eq s1 s2 | CCast(t1,c1), CCast(t2,c2) -> constr_expr_eq t1 t2 && cast_expr_eq c1 c2 | CNotation(n1, s1), CNotation(n2, s2) -> @@ -395,7 +396,7 @@ let map_constr_expr_with_binders g f e = CAst.map (function let (e,bl) = map_local_binders f g e bl in CLambdaN (bl,f e b) | CLetIn (na,a,t,b) -> CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (na.CAst.v) e) b) - | CCast (a,c) -> CCast (f e a, Miscops.map_cast_type (f e) c) + | CCast (a,c) -> CCast (f e a, Glob_ops.map_cast_type (f e) c) | CNotation (n,(l,ll,bl,bll)) -> (* This is an approximation because we don't know what binds what *) CNotation (n,(List.map (f e) l,List.map (List.map (f e)) ll, bl, @@ -545,7 +546,7 @@ let coerce_to_id = function let coerce_to_name = function | { CAst.loc; v = CRef ({v=Ident id},None) } -> CAst.make ?loc @@ Name id - | { CAst.loc; v = CHole (None,Misctypes.IntroAnonymous,None) } -> CAst.make ?loc Anonymous + | { CAst.loc; v = CHole (None,IntroAnonymous,None) } -> CAst.make ?loc Anonymous | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_name" (str "This expression should be a name.") @@ -569,7 +570,7 @@ let mkAppPattern ?loc p lp = let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function | CRef (r,None) -> CPatAtom (Some r) - | CHole (None,Misctypes.IntroAnonymous,None) -> + | CHole (None,IntroAnonymous,None) -> CPatAtom None | CLetIn ({CAst.loc;v=Name id},b,None,{ CAst.v = CRef ({v=Ident id'},None) }) when Id.equal id id' -> CPatAlias (coerce_to_cases_pattern_expr b, CAst.(make ?loc @@ Name id)) diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index b4f0886ac..1c2348457 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -10,7 +10,6 @@ open Names open Libnames -open Misctypes open Constrexpr (** Constrexpr_ops: utilities on [constr_expr] *) @@ -44,7 +43,7 @@ val local_binders_loc : local_binder_expr list -> Loc.t option val mkIdentC : Id.t -> constr_expr val mkRefC : reference -> constr_expr val mkAppC : constr_expr * constr_expr list -> constr_expr -val mkCastC : constr_expr * constr_expr cast_type -> constr_expr +val mkCastC : constr_expr * constr_expr Glob_term.cast_type -> constr_expr val mkLambdaC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr val mkLetInC : lname * constr_expr * constr_expr option * constr_expr -> constr_expr val mkProdC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 86f6ce9ae..c613effcd 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -17,6 +17,7 @@ open Nameops open Termops open Libnames open Globnames +open Namegen open Impargs open CAst open Constrexpr @@ -719,7 +720,7 @@ let extended_glob_local_binder_of_decl loc = function | (p,bk,None,t) -> GLocalAssum (p,bk,t) | (p,bk,Some x, t) -> match DAst.get t with - | GHole (_, Misctypes.IntroAnonymous, None) -> GLocalDef (p,bk,x,None) + | GHole (_, IntroAnonymous, None) -> GLocalDef (p,bk,x,None) | _ -> GLocalDef (p,bk,x,Some t) let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_local_binder_of_decl loc u) @@ -754,13 +755,13 @@ let rec extern inctx scopes vars r = | GVar id -> CRef (make ?loc @@ Ident id,None) - | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, Misctypes.IntroAnonymous, None) + | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, IntroAnonymous, None) | GEvar (n,l) -> extern_evar n (List.map (on_snd (extern false scopes vars)) l) | GPatVar kind -> - if !print_meta_as_hole then CHole (None, Misctypes.IntroAnonymous, None) else + if !print_meta_as_hole then CHole (None, IntroAnonymous, None) else (match kind with | Evar_kinds.SecondOrderPatVar n -> CPatVar n | Evar_kinds.FirstOrderPatVar n -> CEvar (n,[])) @@ -916,7 +917,7 @@ let rec extern inctx scopes vars r = | GCast (c, c') -> CCast (sub_extern true scopes vars c, - Miscops.map_cast_type (extern_typ scopes vars) c') + map_cast_type (extern_typ scopes vars) c') | GProj (p, c) -> let pr = extern_reference ?loc Id.Set.empty (ConstRef (Projection.constant p)) in CProj (pr, sub_extern inctx scopes vars c) @@ -1159,7 +1160,7 @@ let extern_closed_glob ?lax goal_concl_style env sigma t = let any_any_branch = (* | _ => _ *) - CAst.make ([],[DAst.make @@ PatVar Anonymous], DAst.make @@ GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)) + CAst.make ([],[DAst.make @@ PatVar Anonymous], DAst.make @@ GHole (Evar_kinds.InternalHole,IntroAnonymous,None)) let compute_displayed_name_in_pattern sigma avoid na c = let open Namegen in @@ -1183,7 +1184,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with anomaly ~label:"glob_constr_of_pattern" (Pp.str "index to an anonymous variable.") with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in GVar id - | PMeta None -> GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None) + | PMeta None -> GHole (Evar_kinds.InternalHole, IntroAnonymous,None) | PMeta (Some n) -> GPatVar (Evar_kinds.FirstOrderPatVar n) | PProj (p,c) -> GApp (DAst.make @@ GRef (ConstRef (Projection.constant p),None), [glob_of_pat avoid env sigma c]) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 057e10c00..d7345b701 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -14,8 +14,8 @@ open Util open CAst open Names open Nameops -open Constr open Namegen +open Constr open Libnames open Globnames open Impargs @@ -394,7 +394,7 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars env fvs in let bl = List.map CAst.(map (fun id -> - (Name id, b, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None)))) + (Name id, b, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None)))) fvs in let na = match na with @@ -431,7 +431,7 @@ let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function | GLocalAssum (na,bk,t) -> (na,bk,None,t) | GLocalDef (na,bk,c,Some t) -> (na,bk,Some c,t) | GLocalDef (na,bk,c,None) -> - let t = DAst.make ?loc @@ GHole(Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in + let t = DAst.make ?loc @@ GHole(Evar_kinds.BinderType na,IntroAnonymous,None) in (na,bk,Some c,t) | GLocalPattern (_,_,_,_) -> Loc.raise ?loc (Stream.Error "pattern with quote not allowed here") @@ -472,7 +472,7 @@ let intern_local_binder_aux ?(global_level=false) intern ntnvars (env,bl) = func let tyc = match ty with | Some ty -> ty - | None -> CAst.make ?loc @@ CHole(None,Misctypes.IntroAnonymous,None) + | None -> CAst.make ?loc @@ CHole(None,IntroAnonymous,None) in let env, ((disjpat,il),id),na = intern_cases_pattern_as_binder ?loc ntnvars env p in let bk = Default Explicit in @@ -502,11 +502,11 @@ let intern_generalization intern env ntnvars loc bk ak c = if pi then (fun {loc=loc';v=id} acc -> DAst.make ?loc:(Loc.merge_opt loc' loc) @@ - GProd (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc)) + GProd (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None), acc)) else (fun {loc=loc';v=id} acc -> DAst.make ?loc:(Loc.merge_opt loc' loc) @@ - GLambda (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc)) + GLambda (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None), acc)) in List.fold_right (fun ({loc;v=id} as lid) (env, acc) -> let env' = push_name_env ntnvars (Variable,[],[],[]) env CAst.(make @@ Name id) in @@ -564,7 +564,7 @@ let term_of_name = function | Name id -> DAst.make (GVar id) | Anonymous -> let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in - DAst.make (GHole (Evar_kinds.QuestionMark (st,Anonymous), Misctypes.IntroAnonymous, None)) + DAst.make (GHole (Evar_kinds.QuestionMark (st,Anonymous), IntroAnonymous, None)) let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) = function | Anonymous -> (renaming,env), None, Anonymous @@ -626,7 +626,7 @@ let terms_of_binders bl = | PatVar (Anonymous) -> error_cannot_coerce_wildcard_term ?loc () | PatCstr (c,l,_) -> let r = make ?loc @@ Qualid (qualid_of_path (path_of_global (ConstructRef c))) in - let hole = CAst.make ?loc @@ CHole (None,Misctypes.IntroAnonymous,None) in + let hole = CAst.make ?loc @@ CHole (None,IntroAnonymous,None) in let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in CAppExpl ((None,r,None),params @ List.map term_of_pat l)) pt in let rec extract_variables l = match l with @@ -1725,15 +1725,15 @@ let get_implicit_name n imps = let set_hole_implicit i b c = let loc = c.CAst.loc in match DAst.get c with - | GRef (r, _) -> Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None) + | GRef (r, _) -> Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),IntroAnonymous,None) | GApp (r, _) -> let loc = r.CAst.loc in begin match DAst.get r with | GRef (r, _) -> - Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None) + Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),IntroAnonymous,None) | _ -> anomaly (Pp.str "Only refs have implicits.") end - | GVar id -> Loc.tag ?loc (Evar_kinds.ImplicitArg (VarRef id,i,b),Misctypes.IntroAnonymous,None) + | GVar id -> Loc.tag ?loc (Evar_kinds.ImplicitArg (VarRef id,i,b),IntroAnonymous,None) | _ -> anomaly (Pp.str "Only refs have implicits.") let exists_implicit_name id = @@ -1919,13 +1919,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let fields = sort_fields ~complete:true loc fs (fun _idx -> CAst.make ?loc @@ CHole (Some (Evar_kinds.QuestionMark (st,Anonymous)), - Misctypes.IntroAnonymous, None)) + IntroAnonymous, None)) in begin match fields with | None -> user_err ?loc ~hdr:"intern" (str"No constructor inference.") | Some (n, constrname, args) -> - let pars = List.make n (CAst.make ?loc @@ CHole (None, Misctypes.IntroAnonymous, None)) in + let pars = List.make n (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) in let app = CAst.make ?loc @@ CAppExpl ((None, constrname,None), List.rev_append pars args) in intern env app end @@ -1965,12 +1965,12 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let main_sub_eqn = CAst.make @@ ([],thepats, (* "|p1,..,pn" *) Option.cata (intern_type env') - (DAst.make ?loc @@ GHole(Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None)) + (DAst.make ?loc @@ GHole(Evar_kinds.CasesType false,IntroAnonymous,None)) rtnpo) (* "=> P" if there were a return predicate P, and "=> _" otherwise *) in let catch_all_sub_eqn = if List.for_all (irrefutable globalenv) thepats then [] else [CAst.make @@ ([],List.make (List.length thepats) (DAst.make @@ PatVar Anonymous), (* "|_,..,_" *) - DAst.make @@ GHole(Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None))] (* "=> _" *) in + DAst.make @@ GHole(Evar_kinds.ImpossibleCase,IntroAnonymous,None))] (* "=> _" *) in Some (DAst.make @@ GCases(RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn)) in let eqns' = List.map (intern_eqn (List.length tms) env) eqns in @@ -2001,7 +2001,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | None -> let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in (match naming with - | Misctypes.IntroIdentifier id -> Evar_kinds.NamedHole id + | IntroIdentifier id -> Evar_kinds.NamedHole id | _ -> Evar_kinds.QuestionMark (st,Anonymous)) | Some k -> k in @@ -2046,7 +2046,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = GSort s | CCast (c1, c2) -> DAst.make ?loc @@ - GCast (intern env c1, Miscops.map_cast_type (intern_type env) c2) + GCast (intern env c1, map_cast_type (intern_type env) c2) | CProj (pr, c) -> match intern_reference pr with | ConstRef p -> diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index f208b23fb..ab0bf9c6f 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -16,7 +16,7 @@ open Nameops open Constr open Globnames open Decl_kinds -open Misctypes +open Namegen open Glob_term open Glob_ops open Mod_subst @@ -86,7 +86,7 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with Array.equal (eq_notation_constr vars) us1 us2 && Array.equal (eq_notation_constr vars) rs1 rs2 | NSort s1, NSort s2 -> - Miscops.glob_sort_eq s1 s2 + glob_sort_eq s1 s2 | NCast (t1, c1), NCast (t2, c2) -> (eq_notation_constr vars) t1 t2 && cast_type_eq (eq_notation_constr vars) c1 c2 | NProj (p1, c1), NProj (p2, c2) -> @@ -158,7 +158,7 @@ let protect g e na = let apply_cases_pattern ?loc ((ids,disjpat),id) c = let tm = DAst.make ?loc (GVar id) in let eqns = List.map (fun pat -> (CAst.make ?loc (ids,[pat],c))) disjpat in - DAst.make ?loc @@ GCases (LetPatternStyle, None, [tm,(Anonymous,None)], eqns) + DAst.make ?loc @@ GCases (Constr.LetPatternStyle, None, [tm,(Anonymous,None)], eqns) let glob_constr_of_notation_constr_with_binders ?loc g f e nc = let lt x = DAst.make ?loc x in lt @@ match nc with @@ -216,7 +216,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in let e',idl = Array.fold_left_map (to_id (protect g)) e idl in GRec (fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl) - | NCast (c,k) -> GCast (f e c,Miscops.map_cast_type (f e) k) + | NCast (c,k) -> GCast (f e c,map_cast_type (f e) k) | NSort x -> GSort x | NHole (x, naming, arg) -> GHole (x, naming, arg) | NRef x -> GRef (x,None) @@ -434,7 +434,7 @@ let notation_constr_and_vars_of_glob_constr recvars a = user_err Pp.(str "Binders marked as implicit not allowed in notations."); add_name found na; (na,Option.map aux oc,aux b))) dll in NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl) - | GCast (c,k) -> NCast (aux c,Miscops.map_cast_type aux k) + | GCast (c,k) -> NCast (aux c,map_cast_type aux k) | GSort s -> NSort s | GHole (w,naming,arg) -> if arg != None then has_ltac := true; @@ -637,7 +637,7 @@ let rec subst_notation_constr subst bound raw = | NCast (r1,k) -> let r1' = subst_notation_constr subst bound r1 in - let k' = Miscops.smartmap_cast_type (subst_notation_constr subst bound) k in + let k' = smartmap_cast_type (subst_notation_constr subst bound) k in if r1' == r1 && k' == k then raw else NCast(r1',k') | NProj (p, c) -> @@ -666,11 +666,11 @@ let abstract_return_type_context pi mklam tml rtno = let abstract_return_type_context_glob_constr tml rtn = abstract_return_type_context (fun {CAst.v=(_,nal)} -> nal) (fun na c -> DAst.make @@ - GLambda(na,Explicit,DAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None),c)) tml rtn + GLambda(na,Explicit,DAst.make @@ GHole(Evar_kinds.InternalHole,IntroAnonymous,None),c)) tml rtn let abstract_return_type_context_notation_constr tml rtn = abstract_return_type_context snd - (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None),c)) tml rtn + (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, IntroAnonymous, None),c)) tml rtn let is_term_meta id metas = try match Id.List.assoc id metas with _,(NtnTypeConstr | NtnTypeConstrList) -> true | _ -> false @@ -1194,7 +1194,7 @@ let rec match_ inner u alp metas sigma a1 a2 = | GCast(t1, c1), NCast(t2, c2) -> match_cast (match_in u alp metas) (match_in u alp metas sigma t1 t2) c1 c2 | GSort (GType _), NSort (GType _) when not u -> sigma - | GSort s1, NSort s2 when Miscops.glob_sort_eq s1 s2 -> sigma + | GSort s1, NSort s2 when glob_sort_eq s1 s2 -> sigma | GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match | a, NHole _ -> sigma @@ -1208,7 +1208,7 @@ let rec match_ inner u alp metas sigma a1 a2 = let avoid = Id.Set.union (free_glob_vars a1) (* as in Namegen: *) (glob_visible_short_qualid a1) in let id' = Namegen.next_ident_away id avoid in - let t1 = DAst.make @@ GHole(Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in + let t1 = DAst.make @@ GHole(Evar_kinds.BinderType (Name id'),IntroAnonymous,None) in let sigma = match t2 with | NHole _ -> sigma | NVar id2 -> bind_term_env alp sigma id2 t1 @@ -1241,7 +1241,7 @@ and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 = let store, get = set_temporary_memory () in match na1, DAst.get b1, na2 with (* Matching individual binders as part of a recursive pattern *) - | Name p, GCases (LetPatternStyle,None,[(e,_)],(_::_ as eqns)), Name id + | Name p, GCases (Constr.LetPatternStyle,None,[(e,_)],(_::_ as eqns)), Name id when is_gvar p e && is_bindinglist_meta id metas && List.length (store (Detyping.factorize_eqns eqns)) = 1 -> (match get () with | [{CAst.v=(ids,disj_of_patl,b1)}] -> diff --git a/interp/notation_term.ml b/interp/notation_term.ml index 52a6354a0..6d9effcef 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Misctypes open Glob_term (** [notation_constr] *) @@ -25,7 +24,7 @@ type notation_constr = | NRef of GlobRef.t | NVar of Id.t | NApp of notation_constr * notation_constr list - | NHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option + | NHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option | NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool (** Part only in [glob_constr] *) | NLambda of Name.t * notation_constr * notation_constr diff --git a/interp/tactypes.ml b/interp/tactypes.ml index 83e42be89..f19abefee 100644 --- a/interp/tactypes.ml +++ b/interp/tactypes.ml @@ -15,7 +15,35 @@ open Names open Constrexpr open Pattern -open Misctypes + +(** Introduction patterns *) + +type 'constr intro_pattern_expr = + | IntroForthcoming of bool + | IntroNaming of Namegen.intro_pattern_naming_expr + | IntroAction of 'constr intro_pattern_action_expr +and 'constr intro_pattern_action_expr = + | IntroWildcard + | IntroOrAndPattern of 'constr or_and_intro_pattern_expr + | IntroInjection of ('constr intro_pattern_expr) CAst.t list + | IntroApplyOn of 'constr CAst.t * 'constr intro_pattern_expr CAst.t + | IntroRewrite of bool +and 'constr or_and_intro_pattern_expr = + | IntroOrPattern of ('constr intro_pattern_expr) CAst.t list list + | IntroAndPattern of ('constr intro_pattern_expr) CAst.t list + +(** Bindings *) + +type quantified_hypothesis = AnonHyp of int | NamedHyp of Id.t + +type 'a explicit_bindings = (quantified_hypothesis * 'a) CAst.t list + +type 'a bindings = + | ImplicitBindings of 'a list + | ExplicitBindings of 'a explicit_bindings + | NoBindings + +type 'a with_bindings = 'a * 'a bindings (** In globalize tactics, we need to keep the initial [constr_expr] to recompute in the environment by the effective calls to Intro, Inversion, etc @@ -31,4 +59,4 @@ type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_op type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t -type intro_pattern_naming = intro_pattern_naming_expr CAst.t +type intro_pattern_naming = Namegen.intro_pattern_naming_expr CAst.t diff --git a/library/misctypes.ml b/library/misctypes.ml deleted file mode 100644 index 7cd1a83be..000000000 --- a/library/misctypes.ml +++ /dev/null @@ -1,86 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* + | GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),IntroAnonymous,s) -> decr occref; if Int.equal !occref 0 then tc else (incr locref; DAst.make ~loc:(Loc.make_loc (!locref,0)) @@ - GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s)) + GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),IntroAnonymous,s)) | _ -> map_glob_constr_left_to_right substrec c in substrec t diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index ed54320a5..de9ff2875 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -12,9 +12,11 @@ DECLARE PLUGIN "ltac_plugin" open Util open Pp +open Glob_term open Constrexpr open Tacexpr open Misctypes +open Namegen open Genarg open Genredexpr open Tok (* necessary for camlp5 *) diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index 079001ee4..2189e224f 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -11,7 +11,6 @@ (* Syntax for rewriting with strategies *) open Names -open Misctypes open Locus open Constrexpr open Glob_term @@ -20,6 +19,7 @@ open Extraargs open Tacmach open Rewrite open Stdarg +open Tactypes open Pcoq.Prim open Pcoq.Constr open Pvernac.Vernac_ diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 038d55e4b..c91c160f0 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -12,12 +12,14 @@ open Pp open CErrors open Util open Names +open Namegen open Tacexpr open Genredexpr open Constrexpr open Libnames open Tok open Misctypes +open Tactypes open Locus open Decl_kinds diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index de23d2f8e..a75ca8ecb 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -16,6 +16,7 @@ open Constrexpr open Tacexpr open Genredexpr open Misctypes +open Tactypes val open_constr : constr_expr Gram.entry val constr_with_bindings : constr_expr with_bindings Gram.entry diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 894d91258..7b72a4bf9 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -20,6 +20,7 @@ open Stdarg open Libnames open Notation_gram open Misctypes +open Tactypes open Locus open Decl_kinds open Genredexpr @@ -749,7 +750,7 @@ let pr_goal_selector ~toplevel s = | TacIntroPattern (ev,(_::_ as p)) -> hov 1 (primitive (if ev then "eintros" else "intros") ++ (match p with - | [{CAst.v=Misctypes.IntroForthcoming false}] -> mt () + | [{CAst.v=IntroForthcoming false}] -> mt () | _ -> spc () ++ prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)) | TacApply (a,ev,cb,inhyp) -> hov 1 ( diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 5d2a99618..c14874d6c 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -19,6 +19,7 @@ open Environ open Constrexpr open Notation_gram open Tacexpr +open Tactypes type 'a grammar_tactic_prod_item_expr = | TacTerm of string diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index b91315aca..cd04f4ae9 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -26,7 +26,7 @@ open Classes open Constrexpr open Globnames open Evd -open Misctypes +open Tactypes open Locus open Locusops open Decl_kinds @@ -1846,7 +1846,7 @@ let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans = (CAst.make @@ Ident (Id.of_string "Equivalence_Symmetric"), lemma2); (CAst.make @@ Ident (Id.of_string "Equivalence_Transitive"), lemma3)]) -let cHole = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None) +let cHole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) let proper_projection sigma r ty = let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) in diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 1e3d4733b..0d014a0bf 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -12,9 +12,9 @@ open Names open Environ open EConstr open Constrexpr -open Tacexpr -open Misctypes open Evd +open Tactypes +open Tacexpr open Tacinterp (** TODO: document and clean me! *) diff --git a/plugins/ltac/tacarg.mli b/plugins/ltac/tacarg.mli index 59473a5e5..1abe7cd6f 100644 --- a/plugins/ltac/tacarg.mli +++ b/plugins/ltac/tacarg.mli @@ -11,7 +11,7 @@ open Genarg open Tacexpr open Constrexpr -open Misctypes +open Tactypes (** Generic arguments based on Ltac. *) diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 3812a2ba2..27acbb629 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -13,6 +13,8 @@ open Names open Constr open EConstr open Misctypes +open Namegen +open Tactypes open Genarg open Stdarg open Geninterp diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index 5185217cd..31bce197b 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -14,6 +14,7 @@ open EConstr open Misctypes open Genarg open Geninterp +open Tactypes (** Coercions from highest level generic arguments to actual data used by Ltac interpretation. Those functions examinate dynamic types and try to return @@ -56,7 +57,7 @@ val coerce_to_ident_not_fresh : Environ.env -> Evd.evar_map -> Value.t -> Id.t val coerce_to_intro_pattern : Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr val coerce_to_intro_pattern_naming : - Environ.env -> Evd.evar_map -> Value.t -> intro_pattern_naming_expr + Environ.env -> Evd.evar_map -> Value.t -> Namegen.intro_pattern_naming_expr val coerce_to_hint_base : Value.t -> string diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index d6f7a461b..289434d8a 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -16,6 +16,7 @@ open Genredexpr open Genarg open Pattern open Misctypes +open Tactypes open Locus type ltac_constant = KerName.t @@ -75,7 +76,7 @@ type 'id message_token = type ('dconstr,'id) induction_clause = 'dconstr with_bindings Tactics.destruction_arg * - (intro_pattern_naming_expr CAst.t option (* eqn:... *) + (Namegen.intro_pattern_naming_expr CAst.t option (* eqn:... *) * 'dconstr or_and_intro_pattern_expr CAst.t or_var option) (* as ... *) * 'id clause_expr option (* in ... *) @@ -134,7 +135,7 @@ type delayed_open_constr = EConstr.constr delayed_open type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t -type intro_pattern_naming = intro_pattern_naming_expr CAst.t +type intro_pattern_naming = Namegen.intro_pattern_naming_expr CAst.t (** Generic expressions for atomic tactics *) @@ -152,7 +153,7 @@ type 'a gen_atomic_tactic_expr = 'dtrm intro_pattern_expr CAst.t option * 'trm | TacGeneralize of ('trm with_occurrences * Name.t) list | TacLetTac of evars_flag * Name.t * 'trm * 'nam clause_expr * letin_flag * - intro_pattern_naming_expr CAst.t option + Namegen.intro_pattern_naming_expr CAst.t option (* Derived basic tactics *) | TacInductionDestruct of diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index d6f7a461b..42f6883b4 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -17,6 +17,7 @@ open Genarg open Pattern open Misctypes open Locus +open Tactypes type ltac_constant = KerName.t @@ -75,7 +76,7 @@ type 'id message_token = type ('dconstr,'id) induction_clause = 'dconstr with_bindings Tactics.destruction_arg * - (intro_pattern_naming_expr CAst.t option (* eqn:... *) + (Namegen.intro_pattern_naming_expr CAst.t option (* eqn:... *) * 'dconstr or_and_intro_pattern_expr CAst.t or_var option) (* as ... *) * 'id clause_expr option (* in ... *) @@ -134,7 +135,7 @@ type delayed_open_constr = EConstr.constr delayed_open type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t -type intro_pattern_naming = intro_pattern_naming_expr CAst.t +type intro_pattern_naming = Namegen.intro_pattern_naming_expr CAst.t (** Generic expressions for atomic tactics *) @@ -152,7 +153,7 @@ type 'a gen_atomic_tactic_expr = 'dtrm intro_pattern_expr CAst.t option * 'trm | TacGeneralize of ('trm with_occurrences * Name.t) list | TacLetTac of evars_flag * Name.t * 'trm * 'nam clause_expr * letin_flag * - intro_pattern_naming_expr CAst.t option + Namegen.intro_pattern_naming_expr CAst.t option (* Derived basic tactics *) | TacInductionDestruct of diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 9ad9e1520..2a5c38024 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -28,6 +28,8 @@ open Genarg open Stdarg open Tacarg open Misctypes +open Namegen +open Tactypes open Locus (** Globalization of tactic expressions : diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index fb32508cc..9146fced2 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -12,7 +12,7 @@ open Names open Tacexpr open Genarg open Constrexpr -open Misctypes +open Tactypes (** Globalization of tactic expressions : Conversion from [raw_tactic_expr] to [glob_tactic_expr] *) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index a93cf5ae7..04c93eae3 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -12,6 +12,7 @@ open Constrintern open Patternops open Pp open CAst +open Namegen open Genredexpr open Glob_term open Glob_ops @@ -36,6 +37,7 @@ open Tacarg open Printer open Pretyping open Misctypes +open Tactypes open Locus open Tacintern open Taccoerce diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index bd44bdbea..e18f6ab19 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -15,6 +15,7 @@ open Tacexpr open Genarg open Redexpr open Misctypes +open Tactypes val ltac_trace_info : ltac_trace Exninfo.t diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 50bf687b1..0b86a68b0 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -15,6 +15,7 @@ open Genarg open Stdarg open Tacarg open Misctypes +open Tactypes open Globnames open Genredexpr open Patternops diff --git a/plugins/ltac/tacsubst.mli b/plugins/ltac/tacsubst.mli index 0a894791b..d406686c5 100644 --- a/plugins/ltac/tacsubst.mli +++ b/plugins/ltac/tacsubst.mli @@ -11,7 +11,7 @@ open Tacexpr open Mod_subst open Genarg -open Misctypes +open Tactypes (** Substitution of tactics at module closing time *) diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 8eeb8903e..368c20469 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -94,7 +94,7 @@ let clear id = Tactics.clear [id] let assumption = Tactics.assumption -let split = Tactics.split_with_bindings false [Misctypes.NoBindings] +let split = Tactics.split_with_bindings false [Tactypes.NoBindings] (** Test *) @@ -175,7 +175,7 @@ let flatten_contravariant_disj _ ist = | Some (_,args) -> let map i arg = let typ = mkArrow arg c in - let ci = Tactics.constructor_tac false None (succ i) Misctypes.NoBindings in + let ci = Tactics.constructor_tac false None (succ i) Tactypes.NoBindings in let by = tclTHENLIST [intro; apply hyp; ci; assumption] in assert_ ~by typ in diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 68620dbfc..f22147f8b 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -23,6 +23,7 @@ open Names open Goptions open Mutils open Constr +open Tactypes (** * Debug flag @@ -1727,7 +1728,7 @@ let micromega_gen let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in - let ipat_of_name id = Some (CAst.make @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in + let ipat_of_name id = Some (CAst.make @@ IntroNaming (Namegen.IntroIdentifier id)) in let goal_name = fresh_id Id.Set.empty (Names.Id.of_string "__arith") gl in let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in @@ -1842,7 +1843,7 @@ let micromega_genr prover tac = let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in - let ipat_of_name id = Some (CAst.make @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in + let ipat_of_name id = Some (CAst.make @@ IntroNaming (Namegen.IntroIdentifier id)) in let goal_name = fresh_id Id.Set.empty (Names.Id.of_string "__arith") gl in let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index c615cf278..6f4138828 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -29,7 +29,7 @@ open Libnames open Globnames open Nametab open Contradiction -open Misctypes +open Tactypes open Context.Named.Declaration module NamedDecl = Context.Named.Declaration diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 3f6503e73..ea7216832 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -184,7 +184,7 @@ open Globnames open Misctypes open Decl_kinds -let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None) +let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) let rec mkRHoles n = if n > 0 then mkRHole :: mkRHoles (n - 1) else [] let rec isRHoles cl = match cl with @@ -254,7 +254,7 @@ let interp_refine ist gl rc = let interp_open_constr ist gl gc = - let (sigma, (c, _)) = Tacinterp.interp_open_constr_with_bindings ist (pf_env gl) (project gl) (gc, Misctypes.NoBindings) in + let (sigma, (c, _)) = Tacinterp.interp_open_constr_with_bindings ist (pf_env gl) (project gl) (gc, Tactypes.NoBindings) in (project gl, (sigma, c)) let interp_term ist gl (_, c) = snd (interp_open_constr ist gl c) @@ -861,8 +861,8 @@ let mkCProp loc = CAst.make ?loc @@ CSort GProp let mkCType loc = CAst.make ?loc @@ CSort (GType []) let mkCVar ?loc id = CAst.make ?loc @@ CRef (CAst.make ?loc @@ Ident id, None) let rec mkCHoles ?loc n = - if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) :: mkCHoles ?loc (n - 1) -let mkCHole loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None) + if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None)) :: mkCHoles ?loc (n - 1) +let mkCHole loc = CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None) let mkCLambda ?loc name ty t = CAst.make ?loc @@ CLambdaN ([CLocalAssum([CAst.make ?loc name], Default Explicit, ty)], t) let mkCArrow ?loc ty t = CAst.make ?loc @@ diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 83b4d6562..fbe3b000f 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -17,7 +17,7 @@ open Term open Constr open Termops open Globnames -open Misctypes +open Tactypes open Tacmach open Ssrmatching_plugin diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index c6beb08c5..2c046190f 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -86,7 +86,6 @@ let _ = open Constrexpr open Glob_term -open Misctypes let combineCG t1 t2 f g = match t1, t2 with | (x, (t1, None)), (_, (t2, None)) -> x, (g t1 t2, None) diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index fbfbdb110..9d7fc254c 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -29,6 +29,8 @@ open Extraargs open Ppconstr open Misctypes +open Namegen +open Tactypes open Decl_kinds open Constrexpr open Constrexpr_ops @@ -543,7 +545,7 @@ END let remove_loc x = x.CAst.v -let ipat_of_intro_pattern p = Misctypes.( +let ipat_of_intro_pattern p = Tactypes.( let rec ipat_of_intro_pattern = function | IntroNaming (IntroIdentifier id) -> IPatId id | IntroAction IntroWildcard -> IPatAnon Drop @@ -595,16 +597,15 @@ let intern_ipats ist = List.map (intern_ipat ist) let interp_intro_pattern = interp_wit wit_intro_pattern -let interp_introid ist gl id = Misctypes.( +let interp_introid ist gl id = try IntroNaming (IntroIdentifier (hyp_id (snd (interp_hyp ist gl (SsrHyp (Loc.tag id)))))) with _ -> (snd (interp_intro_pattern ist gl (CAst.make @@ IntroNaming (IntroIdentifier id)))).CAst.v -) let get_intro_id = function | IntroNaming (IntroIdentifier id) -> id | _ -> assert false -let rec add_intro_pattern_hyps ipat hyps = Misctypes.( +let rec add_intro_pattern_hyps ipat hyps = let {CAst.loc=loc;v=ipat} = ipat in match ipat with | IntroNaming (IntroIdentifier id) -> @@ -623,7 +624,6 @@ let rec add_intro_pattern_hyps ipat hyps = Misctypes.( | IntroForthcoming _ -> (* As in ipat_of_intro_pattern, was unable to determine which kind of ipat interp_introid could return [HH] *) assert false -) (* We interp the ipat using the standard ltac machinery for ids, since * we have no clue what a name could be bound to (maybe another ipat) *) @@ -1064,7 +1064,7 @@ let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with | BFdef :: h, { v = CLetIn({CAst.v=x}, v, oty, c) } -> let bs, c' = format_constr_expr h c in Bdef (x, oty, v) :: bs, c' - | [BFcast], { v = CCast (c, CastConv t) } -> + | [BFcast], { v = CCast (c, Glob_term.CastConv t) } -> [Bcast t], c | BFrec (has_str, has_cast) :: h, { v = CFix ( _, [_, (Some locn, CStructRec), bl, t, c]) } -> @@ -1093,7 +1093,7 @@ let wit_ssrfwdfmt = add_genarg "ssrfwdfmt" pr_fwdfmt let mkFwdVal fk c = ((fk, []), c) let mkssrFwdVal fk c = ((fk, []), (c,None)) -let dC t = CastConv t +let dC t = Glob_term.CastConv t let same_ist { interp_env = x } { interp_env = y } = match x,y with @@ -1210,8 +1210,8 @@ let push_binders c2 bs = | [] -> c | _ -> anomaly "binder not a lambda nor a let in" in match c2 with - | { loc; v = CCast (ct, CastConv cty) } -> - CAst.make ?loc @@ (CCast (loop false ct bs, CastConv (loop true cty bs))) + | { loc; v = CCast (ct, Glob_term.CastConv cty) } -> + CAst.make ?loc @@ (CCast (loop false ct bs, Glob_term.CastConv (loop true cty bs))) | ct -> loop false ct bs let rec fix_binders = let open CAst in function diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 29a936381..faebe3179 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -157,7 +157,7 @@ let tclINJ_CONSTR_IST ist p = let mkGHole = DAst.make - (Glob_term.GHole(Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None)) + (Glob_term.GHole(Evar_kinds.InternalHole, Namegen.IntroAnonymous, None)) let rec mkGHoles n = if n > 0 then mkGHole :: mkGHoles (n - 1) else [] let mkGApp f args = if args = [] then f diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index b1c5e131f..69d944fa1 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -40,7 +40,7 @@ open Pretyping open Ppconstr open Printer open Globnames -open Misctypes +open Namegen open Decl_kinds open Evar_kinds open Constrexpr diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 1edce17bd..aa1c23f52 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -2103,7 +2103,7 @@ let mk_JMeq_refl evdref typ x = let hole na = DAst.make @@ GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false,na), - Misctypes.IntroAnonymous, None) + IntroAnonymous, None) let constr_of_pat env evdref arsign pat avoid = let rec typ env (ty, realargs) pat avoid = diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index e6cfe1f76..df89d9eac 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -27,7 +27,6 @@ open Libnames open Globnames open Nametab open Mod_subst -open Misctypes open Decl_kinds open Context.Named.Declaration open Ltac_pretype @@ -1027,7 +1026,7 @@ let rec subst_glob_constr subst = DAst.map (function | GCast (r1,k) as raw -> let r1' = subst_glob_constr subst r1 in - let k' = Miscops.smartmap_cast_type (subst_glob_constr subst) k in + let k' = smartmap_cast_type (subst_glob_constr subst) k in if r1' == r1 && k' == k then raw else GCast (r1',k') | GProj (p,c) as raw -> diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 63618c918..71a457280 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -11,10 +11,8 @@ open Util open CAst open Names -open Constr open Nameops open Globnames -open Misctypes open Glob_term open Evar_kinds open Ltac_pretype @@ -48,12 +46,20 @@ let map_glob_decl_left_to_right f (na,k,obd,ty) = let comp2 = f ty in (na,k,comp1,comp2) + +let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with +| GProp, GProp -> true +| GSet, GSet -> true +| GType l1, GType l2 -> + List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.eq_reference x y && Int.equal m n)) l1 l2 +| _ -> false + let binding_kind_eq bk1 bk2 = match bk1, bk2 with | Decl_kinds.Explicit, Decl_kinds.Explicit -> true | Decl_kinds.Implicit, Decl_kinds.Implicit -> true | (Decl_kinds.Explicit | Decl_kinds.Implicit), _ -> false -let case_style_eq s1 s2 = match s1, s2 with +let case_style_eq s1 s2 = let open Constr in match s1, s2 with | LetStyle, LetStyle -> true | IfStyle, IfStyle -> true | LetPatternStyle, LetPatternStyle -> true @@ -141,10 +147,10 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with fix_kind_eq f kn1 kn2 && Array.equal Id.equal id1 id2 && Array.equal (fun l1 l2 -> List.equal (glob_decl_eq f) l1 l2) decl1 decl2 && Array.equal f c1 c2 && Array.equal f t1 t2 - | GSort s1, GSort s2 -> Miscops.glob_sort_eq s1 s2 + | GSort s1, GSort s2 -> glob_sort_eq s1 s2 | GHole (kn1, nam1, gn1), GHole (kn2, nam2, gn2) -> Option.equal (==) gn1 gn2 (** Only thing sensible *) && - Miscops.intro_pattern_naming_eq nam1 nam2 + Namegen.intro_pattern_naming_eq nam1 nam2 | GCast (c1, t1), GCast (c2, t2) -> f c1 c2 && cast_type_eq f t1 t2 | GProj (p1, t1), GProj (p2, t2) -> @@ -154,6 +160,21 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c +(** Mapping [cast_type] *) + +let map_cast_type f = function + | CastConv a -> CastConv (f a) + | CastVM a -> CastVM (f a) + | CastCoerce -> CastCoerce + | CastNative a -> CastNative (f a) + +let smartmap_cast_type f c = + match c with + | CastConv a -> let a' = f a in if a' == a then c else CastConv a' + | CastVM a -> let a' = f a in if a' == a then c else CastVM a' + | CastCoerce -> CastCoerce + | CastNative a -> let a' = f a in if a' == a then c else CastNative a' + let map_glob_constr_left_to_right f = DAst.map (function | GApp (g,args) -> let comp1 = f g in @@ -194,7 +215,7 @@ let map_glob_constr_left_to_right f = DAst.map (function GRec (fk,idl,comp1,comp2,comp3) | GCast (c,k) -> let comp1 = f c in - let comp2 = Miscops.map_cast_type f k in + let comp2 = map_cast_type f k in GCast (comp1,comp2) | GProj (p,c) -> GProj (p, f c) @@ -539,7 +560,7 @@ let rec glob_constr_of_cases_pattern_aux isclosed x = DAst.map_with_loc (fun ?lo | PatVar (Name id) when not isclosed -> GVar id | PatVar Anonymous when not isclosed -> - GHole (Evar_kinds.QuestionMark (Define false,Anonymous),Misctypes.IntroAnonymous,None) + GHole (Evar_kinds.QuestionMark (Define false,Anonymous),Namegen.IntroAnonymous,None) | _ -> raise Not_found ) x diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 124440f5d..c967f4e88 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -13,6 +13,8 @@ open Glob_term (** Equalities *) +val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool + val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool val alias_of_pat : 'a cases_pattern_g -> Name.t @@ -20,10 +22,15 @@ val alias_of_pat : 'a cases_pattern_g -> Name.t val set_pat_alias : Id.t -> 'a cases_pattern_g -> 'a cases_pattern_g val cast_type_eq : ('a -> 'a -> bool) -> - 'a Misctypes.cast_type -> 'a Misctypes.cast_type -> bool + 'a cast_type -> 'a cast_type -> bool val glob_constr_eq : 'a glob_constr_g -> 'a glob_constr_g -> bool +(** Mapping [cast_type] *) + +val map_cast_type : ('a -> 'b) -> 'a cast_type -> 'b cast_type +val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type + (** Operations on [glob_constr] *) val cases_pattern_loc : 'a cases_pattern_g -> Loc.t option diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 6ecb479e6..54fa5328f 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -18,7 +18,6 @@ open Names open Decl_kinds -open Misctypes type existential_name = Id.t @@ -41,6 +40,14 @@ type glob_constraint = glob_level * Univ.constraint_type * glob_level type sort_info = (Libnames.reference * int) option list type glob_sort = sort_info glob_sort_gen +(** Casts *) + +type 'a cast_type = + | CastConv of 'a + | CastVM of 'a + | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *) + | CastNative of 'a + (** The kind of patterns that occurs in "match ... with ... end" locs here refers to the ident's location, not whole pat *) @@ -73,7 +80,7 @@ type 'a glob_constr_r = | GRec of 'a fix_kind_g * Id.t array * 'a glob_decl_g list array * 'a glob_constr_g array * 'a glob_constr_g array | GSort of glob_sort - | GHole of Evar_kinds.t * intro_pattern_naming_expr * Genarg.glob_generic_argument option + | GHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option | GCast of 'a glob_constr_g * 'a glob_constr_g cast_type | GProj of Projection.t * 'a glob_constr_g and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml deleted file mode 100644 index 1697e54ab..000000000 --- a/pretyping/miscops.ml +++ /dev/null @@ -1,55 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* CastConv (f a) - | CastVM a -> CastVM (f a) - | CastCoerce -> CastCoerce - | CastNative a -> CastNative (f a) - -let smartmap_cast_type f c = - match c with - | CastConv a -> let a' = f a in if a' == a then c else CastConv a' - | CastVM a -> let a' = f a in if a' == a then c else CastVM a' - | CastCoerce -> CastCoerce - | CastNative a -> let a' = f a in if a' == a then c else CastNative a' - -(** Equalities on [glob_sort] *) - -let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with -| GProp, GProp -> true -| GSet, GSet -> true -| GType l1, GType l2 -> - List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.eq_reference x y && Int.equal m n)) l1 l2 -| _ -> false - -let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with -| IntroAnonymous, IntroAnonymous -> true -| IntroIdentifier id1, IntroIdentifier id2 -> Names.Id.equal id1 id2 -| IntroFresh id1, IntroFresh id2 -> Names.Id.equal id1 id2 -| _ -> false - -(** Mapping bindings *) - -let map_explicit_bindings f l = - let map = CAst.map (fun (hyp, x) -> (hyp, f x)) in - List.map map l - -let map_bindings f = function -| ImplicitBindings l -> ImplicitBindings (List.map f l) -| ExplicitBindings expl -> ExplicitBindings (map_explicit_bindings f expl) -| NoBindings -> NoBindings - -let map_with_bindings f (x, bl) = (f x, map_bindings f bl) diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli deleted file mode 100644 index 6a84fb9eb..000000000 --- a/pretyping/miscops.mli +++ /dev/null @@ -1,30 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* 'b) -> 'a cast_type -> 'b cast_type -val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type - -(** Equalities on [glob_sort] *) - -val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool - -(** Equalities on [intro_pattern_naming] *) - -val intro_pattern_naming_eq : - intro_pattern_naming_expr -> intro_pattern_naming_expr -> bool - -(** Mapping bindings *) - -val map_bindings : ('a -> 'b) -> 'a bindings -> 'b bindings -val map_with_bindings : ('a -> 'b) -> 'a with_bindings -> 'b with_bindings diff --git a/pretyping/misctypes.ml b/pretyping/misctypes.ml new file mode 100644 index 000000000..c66c9b1b8 --- /dev/null +++ b/pretyping/misctypes.ml @@ -0,0 +1,37 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* + | CHole (_,IntroIdentifier id,_) -> return (str "?[" ++ pr_id id ++ str "]", latom) - | CHole (_,Misctypes.IntroFresh id,_) -> + | CHole (_,IntroFresh id,_) -> return (str "?[?" ++ pr_id id ++ str "]", latom) | CHole (_,_,_) -> return (str "_", latom) diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 450fcddfd..79b7e1599 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -26,7 +26,7 @@ open Tacred open Pretype_errors open Evarutil open Unification -open Misctypes +open Tactypes (******************************************************************) (* Clausal environments *) diff --git a/proofs/clenv.mli b/proofs/clenv.mli index b85c4fc51..f9506290a 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -18,7 +18,7 @@ open Environ open Evd open EConstr open Unification -open Misctypes +open Tactypes (** {6 The Type of Constructions clausale environments.} *) diff --git a/proofs/logic.ml b/proofs/logic.ml index 95c30d815..e8ca71993 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -23,7 +23,6 @@ open Typing open Proof_type open Type_errors open Retyping -open Misctypes module NamedDecl = Context.Named.Declaration @@ -185,6 +184,22 @@ let check_decl_position env sigma sign d = * on the right side [right] if [toleft=false]. * If [with_dep] then dependent hypotheses are moved accordingly. *) +(** Move destination for hypothesis *) + +type 'id move_location = + | MoveAfter of 'id + | MoveBefore of 'id + | MoveFirst + | MoveLast (** can be seen as "no move" when doing intro *) + +(** Printing of [move_location] *) + +let pr_move_location pr_id = function + | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id + | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id + | MoveFirst -> str " at top" + | MoveLast -> str " at bottom" + let move_location_eq m1 m2 = match m1, m2 with | MoveAfter id1, MoveAfter id2 -> Id.equal id1 id2 | MoveBefore id1, MoveBefore id2 -> Id.equal id1 id2 @@ -236,7 +251,7 @@ let move_hyp sigma toleft (left,declfrom,right) hto = (first, d::middle) else user_err ~hdr:"move_hyp" (str "Cannot move " ++ Id.print (NamedDecl.get_id declfrom) ++ - Miscprint.pr_move_location Id.print hto ++ + pr_move_location Id.print hto ++ str (if toleft then ": it occurs in the type of " else ": it depends on ") ++ Id.print hyp ++ str ".") else diff --git a/proofs/logic.mli b/proofs/logic.mli index dc471bb5f..9db54732b 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -58,12 +58,23 @@ val error_no_such_hypothesis : Environ.env -> evar_map -> Id.t -> 'a val catchable_exception : exn -> bool +(** Move destination for hypothesis *) + +type 'id move_location = + | MoveAfter of 'id + | MoveBefore of 'id + | MoveFirst + | MoveLast (** can be seen as "no move" when doing intro *) + +val pr_move_location : + ('a -> Pp.t) -> 'a move_location -> Pp.t + val convert_hyp : bool -> Environ.named_context_val -> evar_map -> EConstr.named_declaration -> Environ.named_context_val -val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t Misctypes.move_location -> +val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t move_location -> Environ.named_context_val -> Environ.named_context_val val insert_decl_in_named_context : Evd.evar_map -> - EConstr.named_declaration -> Id.t Misctypes.move_location -> + EConstr.named_declaration -> Id.t move_location -> Environ.named_context_val -> Environ.named_context_val diff --git a/proofs/miscprint.ml b/proofs/miscprint.ml index 1a63ff673..ec17b8076 100644 --- a/proofs/miscprint.ml +++ b/proofs/miscprint.ml @@ -10,7 +10,7 @@ open Pp open Names -open Misctypes +open Tactypes (** Printing of [intro_pattern] *) @@ -20,7 +20,7 @@ let rec pr_intro_pattern prc {CAst.v=pat} = match pat with | IntroNaming p -> pr_intro_pattern_naming p | IntroAction p -> pr_intro_pattern_action prc p -and pr_intro_pattern_naming = function +and pr_intro_pattern_naming = let open Namegen in function | IntroIdentifier id -> Id.print id | IntroFresh id -> str "?" ++ Id.print id | IntroAnonymous -> str "?" @@ -43,14 +43,6 @@ and pr_or_and_intro_pattern prc = function hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc (pr_intro_pattern prc)) pll) ++ str "]" -(** Printing of [move_location] *) - -let pr_move_location pr_id = function - | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id - | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id - | MoveFirst -> str " at top" - | MoveLast -> str " at bottom" - (** Printing of bindings *) let pr_binding prc = let open CAst in function | {loc;v=(NamedHyp id, c)} -> hov 1 (Names.Id.print id ++ str " := " ++ cut () ++ prc c) diff --git a/proofs/miscprint.mli b/proofs/miscprint.mli index 79790a277..f4e2e683d 100644 --- a/proofs/miscprint.mli +++ b/proofs/miscprint.mli @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Misctypes +open Tactypes (** Printing of [intro_pattern] *) @@ -18,13 +18,10 @@ val pr_intro_pattern : val pr_or_and_intro_pattern : ('a -> Pp.t) -> 'a or_and_intro_pattern_expr -> Pp.t -val pr_intro_pattern_naming : intro_pattern_naming_expr -> Pp.t +val pr_intro_pattern_naming : Namegen.intro_pattern_naming_expr -> Pp.t (** Printing of [move_location] *) -val pr_move_location : - ('a -> Pp.t) -> 'a move_location -> Pp.t - val pr_bindings : ('a -> Pp.t) -> ('a -> Pp.t) -> 'a bindings -> Pp.t diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index b92bc75bc..e12063fd4 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -14,7 +14,6 @@ open Hipattern open Tactics open Coqlib open Reductionops -open Misctypes open Proofview.Notations module NamedDecl = Context.Named.Declaration @@ -120,7 +119,7 @@ let contradiction_term (c,lbind as cl) = else Proofview.tclORELSE begin - if lbind = NoBindings then + if lbind = Tactypes.NoBindings then filter_hyp (fun c -> is_negation_of env sigma typ c) (fun id -> simplest_elim (mkApp (mkVar id,[|c|]))) else diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli index 2b3a94758..4bb3263fb 100644 --- a/tactics/contradiction.mli +++ b/tactics/contradiction.mli @@ -9,7 +9,7 @@ (************************************************************************) open EConstr -open Misctypes +open Tactypes val absurd : constr -> unit Proofview.tactic val contradiction : constr with_bindings option -> unit Proofview.tactic diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 176701d99..832014a61 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -24,11 +24,11 @@ open Tactics open Tacticals.New open Auto open Constr_matching -open Misctypes open Hipattern open Proofview.Notations open Tacmach.New open Coqlib +open Tactypes (* This file containts the implementation of the tactics ``Decide Equality'' and ``Compare''. They can be used to decide the @@ -58,14 +58,14 @@ let clear_last = let choose_eq eqonleft = if eqonleft then - left_with_bindings false Misctypes.NoBindings + left_with_bindings false NoBindings else - right_with_bindings false Misctypes.NoBindings + right_with_bindings false NoBindings let choose_noteq eqonleft = if eqonleft then - right_with_bindings false Misctypes.NoBindings + right_with_bindings false NoBindings else - left_with_bindings false Misctypes.NoBindings + left_with_bindings false NoBindings (* A surgical generalize which selects the right occurrences by hand *) (* This prevents issues where c2 is also a subterm of c1 (see e.g. #5449) *) diff --git a/tactics/equality.ml b/tactics/equality.ml index c91758787..1033c56c9 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -43,6 +43,7 @@ open Eqschemes open Locus open Locusops open Misctypes +open Tactypes open Proofview.Notations open Unification open Context.Named.Declaration diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 5d264058a..f9c4bed35 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -263,7 +263,7 @@ open Evar_kinds let mkPattern c = snd (Patternops.pattern_of_glob_constr c) let mkGApp f args = DAst.make @@ GApp (f, args) let mkGHole = DAst.make @@ - GHole (QuestionMark (Define false,Anonymous), Misctypes.IntroAnonymous, None) + GHole (QuestionMark (Define false,Anonymous), Namegen.IntroAnonymous, None) let mkGProd id c1 c2 = DAst.make @@ GProd (Name (Id.of_string id), Explicit, c1, c2) let mkGArrow c1 c2 = DAst.make @@ diff --git a/tactics/inv.ml b/tactics/inv.ml index 102b8e54d..755494c2d 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -26,7 +26,7 @@ open Tacticals.New open Tactics open Elim open Equality -open Misctypes +open Tactypes open Proofview.Notations module NamedDecl = Context.Named.Declaration @@ -332,7 +332,7 @@ let rec tclMAP_i allow_conj n tacfun = function (tacfun (get_names allow_conj a)) (tclMAP_i allow_conj (n-1) tacfun l) -let remember_first_eq id x = if !x == MoveLast then x := MoveAfter id +let remember_first_eq id x = if !x == Logic.MoveLast then x := Logic.MoveAfter id (* invariant: ProjectAndApply is responsible for erasing the clause which it is given as input @@ -375,7 +375,7 @@ let projectAndApply as_mode thin avoid id eqname names depids = [if as_mode then clear [id] else tclIDTAC; (tclMAP_i (false,false) neqns (function (idopt,_) -> tclTRY (tclTHEN - (intro_move_avoid idopt avoid MoveLast) + (intro_move_avoid idopt avoid Logic.MoveLast) (* try again to substitute and if still not a variable after *) (* decomposition, arbitrarily try to rewrite RL !? *) (tclTRY (onLastHypId (substHypIfVariable (fun id -> subst_hyp false id)))))) @@ -404,7 +404,7 @@ let nLastDecls i tac = let rewrite_equations as_mode othin neqns names ba = Proofview.Goal.enter begin fun gl -> let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in - let first_eq = ref MoveLast in + let first_eq = ref Logic.MoveLast in let avoid = if as_mode then Id.Set.of_list (List.map NamedDecl.get_id nodepids) else Id.Set.empty in match othin with | Some thin -> @@ -416,20 +416,20 @@ let rewrite_equations as_mode othin neqns names ba = (nLastDecls neqns (fun ctx -> clear (ids_of_named_context ctx))); tclMAP_i (true,false) neqns (fun (idopt,names) -> (tclTHEN - (intro_move_avoid idopt avoid MoveLast) + (intro_move_avoid idopt avoid Logic.MoveLast) (onLastHypId (fun id -> tclTRY (projectAndApply as_mode thin avoid id first_eq names depids))))) names; tclMAP (fun d -> tclIDTAC >>= fun () -> (* delay for [first_eq]. *) let idopt = if as_mode then Some (NamedDecl.get_id d) else None in - intro_move idopt (if thin then MoveLast else !first_eq)) + intro_move idopt (if thin then Logic.MoveLast else !first_eq)) nodepids; (tclMAP (fun d -> tclTRY (clear [NamedDecl.get_id d])) depids)] | None -> (* simple inversion *) if as_mode then tclMAP_i (false,true) neqns (fun (idopt,_) -> - intro_move idopt MoveLast) names + intro_move idopt Logic.MoveLast) names else (tclTHENLIST [tclDO neqns intro; diff --git a/tactics/inv.mli b/tactics/inv.mli index 9d4ffdd7b..bbd1f3352 100644 --- a/tactics/inv.mli +++ b/tactics/inv.mli @@ -10,7 +10,6 @@ open Names open EConstr -open Misctypes open Tactypes type inversion_status = Dep of constr option | NoDep diff --git a/tactics/leminv.mli b/tactics/leminv.mli index 2337a7901..f42e5a8b0 100644 --- a/tactics/leminv.mli +++ b/tactics/leminv.mli @@ -11,7 +11,7 @@ open Names open EConstr open Constrexpr -open Misctypes +open Tactypes val lemInv_clause : quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 732d06f8a..53a02f89b 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -159,8 +159,6 @@ type branch_assumptions = { ba : branch_args; (* the branch args *) assums : named_context} (* the list of assumptions introduced *) -open Misctypes - let fix_empty_or_and_pattern nv l = (* 1- The syntax does not distinguish between "[ ]" for one clause with no names and "[ ]" for no clause at all *) @@ -194,7 +192,7 @@ let check_or_and_pattern_size ?loc check_and names branchsigns = if not (Int.equal p p1 || Int.equal p p2) then err1 p1 p2; if Int.equal p p1 then IntroAndPattern - (List.extend branchsigns.(0) (CAst.make @@ IntroNaming IntroAnonymous) l) + (List.extend branchsigns.(0) (CAst.make @@ IntroNaming Namegen.IntroAnonymous) l) else names else diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b571b347d..cf07532c0 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -44,6 +44,7 @@ open Unification open Locus open Locusops open Misctypes +open Tactypes open Proofview.Notations open Context.Named.Declaration diff --git a/tactics/tactics.mli b/tactics/tactics.mli index b17330f13..086442e42 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -56,8 +56,8 @@ val find_intro_names : rel_context -> goal sigma -> Id.t list val intro : unit Proofview.tactic val introf : unit Proofview.tactic -val intro_move : Id.t option -> Id.t move_location -> unit Proofview.tactic -val intro_move_avoid : Id.t option -> Id.Set.t -> Id.t move_location -> unit Proofview.tactic +val intro_move : Id.t option -> Id.t Logic.move_location -> unit Proofview.tactic +val intro_move_avoid : Id.t option -> Id.Set.t -> Id.t Logic.move_location -> unit Proofview.tactic (** [intro_avoiding idl] acts as intro but prevents the new Id.t to belong to [idl] *) @@ -117,11 +117,11 @@ val use_clear_hyp_by_default : unit -> bool (** {6 Introduction tactics with eliminations. } *) val intro_patterns : evars_flag -> intro_patterns -> unit Proofview.tactic -val intro_patterns_to : evars_flag -> Id.t move_location -> intro_patterns -> +val intro_patterns_to : evars_flag -> Id.t Logic.move_location -> intro_patterns -> unit Proofview.tactic -val intro_patterns_bound_to : evars_flag -> int -> Id.t move_location -> intro_patterns -> +val intro_patterns_bound_to : evars_flag -> int -> Id.t Logic.move_location -> intro_patterns -> unit Proofview.tactic -val intro_pattern_to : evars_flag -> Id.t move_location -> delayed_open_constr intro_pattern_expr -> +val intro_pattern_to : evars_flag -> Id.t Logic.move_location -> delayed_open_constr intro_pattern_expr -> unit Proofview.tactic (** Implements user-level "intros", with [] standing for "**" *) @@ -188,7 +188,7 @@ val apply_clear_request : clear_flag -> bool -> constr -> unit Proofview.tactic val specialize : constr with_bindings -> intro_pattern option -> unit Proofview.tactic -val move_hyp : Id.t -> Id.t move_location -> unit Proofview.tactic +val move_hyp : Id.t -> Id.t Logic.move_location -> unit Proofview.tactic val rename_hyp : (Id.t * Id.t) list -> unit Proofview.tactic val revert : Id.t list -> unit Proofview.tactic diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 8b56275c7..ee578669c 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -24,7 +24,8 @@ open Globnames open Inductiveops open Tactics open Ind_tables -open Misctypes +open Namegen +open Tactypes open Proofview.Notations module RelDecl = Context.Rel.Declaration diff --git a/vernac/classes.ml b/vernac/classes.ml index 946a7bb32..8cf3895fb 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -145,7 +145,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) (fun avoid (clname, _) -> match clname with | Some cl -> - let t = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None) in + let t = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) in t, avoid | None -> failwith ("new instance: under-applied typeclass")) cl @@ -255,7 +255,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) k.cl_projs; c :: props, rest' with Not_found -> - ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Misctypes.IntroAnonymous, None)) :: props), rest + ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Namegen.IntroAnonymous, None)) :: props), rest else props, rest) ([], props) k.cl_props in diff --git a/vernac/g_proofs.ml4 b/vernac/g_proofs.ml4 index a3806ff68..4b11276af 100644 --- a/vernac/g_proofs.ml4 +++ b/vernac/g_proofs.ml4 @@ -8,10 +8,10 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Glob_term open Constrexpr open Vernacexpr open Proof_global -open Misctypes open Pcoq open Pcoq.Prim diff --git a/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4 index b6523981c..59449d07a 100644 --- a/vernac/g_vernac.ml4 +++ b/vernac/g_vernac.ml4 @@ -12,6 +12,7 @@ open Pp open CErrors open Util open Names +open Glob_term open Vernacexpr open Constrexpr open Constrexpr_ops @@ -20,6 +21,7 @@ open Decl_kinds open Declaremods open Declarations open Misctypes +open Namegen open Tok (* necessary for camlp5 *) open Pcoq @@ -338,7 +340,7 @@ GEXTEND Gram ; type_cstr: [ [ ":"; c=lconstr -> c - | -> CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None) ] ] + | -> CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None) ] ] ; (* Inductive schemes *) scheme: @@ -394,7 +396,7 @@ GEXTEND Gram (None,DefExpr(id,mkCLambdaN ~loc:!@loc l b,None)) ] ] ; record_binder: - [ [ id = name -> (None,AssumExpr(id, CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None))) + [ [ id = name -> (None,AssumExpr(id, CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None))) | id = name; f = record_binder_body -> f id ] ] ; assum_list: @@ -413,7 +415,7 @@ GEXTEND Gram t= [ coe = of_type_with_opt_coercion; c = lconstr -> fun l id -> (not (Option.is_empty coe),(id,mkCProdN ~loc:!@loc l c)) | -> - fun l id -> (false,(id,mkCProdN ~loc:!@loc l (CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None)))) ] + fun l id -> (false,(id,mkCProdN ~loc:!@loc l (CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None)))) ] -> t l ]] ; diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 5490b9ce5..d0c423650 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -286,7 +286,7 @@ open Pputils prlist_strict (pr_module_vardecls pr_c) l let pr_type_option pr_c = function - | { v = CHole (k, Misctypes.IntroAnonymous, _) } -> mt() + | { v = CHole (k, Namegen.IntroAnonymous, _) } -> mt() | _ as c -> brk(0,2) ++ str" :" ++ pr_c c let pr_decl_notation prc ({loc; v=ntn},c,scopt) = diff --git a/vernac/record.ml b/vernac/record.ml index e6a3afe4e..940859723 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -96,7 +96,7 @@ let binder_of_decl = function | Vernacexpr.AssumExpr(n,t) -> (n,None,t) | Vernacexpr.DefExpr(n,c,t) -> (n,Some c, match t with Some c -> c - | None -> CAst.make ?loc:n.CAst.loc @@ CHole (None, Misctypes.IntroAnonymous, None)) + | None -> CAst.make ?loc:n.CAst.loc @@ CHole (None, Namegen.IntroAnonymous, None)) let binders_of_decls = List.map binder_of_decl -- cgit v1.2.3 From 18aac5cdc6ce8be8c5c88d284cd10e82814cb303 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 22 May 2018 04:57:00 +0200 Subject: [api] Misctypes removal: move Tactypes to proofs This gets `Tactypes` closer to `tactics/`, however some legacy stuff blocks it in `proofs`. We consider that is satisfactory for now. --- interp/genintern.ml | 8 +++++- interp/genintern.mli | 8 +++++- interp/stdarg.ml | 13 ---------- interp/stdarg.mli | 23 +--------------- interp/tactypes.ml | 62 -------------------------------------------- plugins/funind/g_indfun.ml4 | 1 + plugins/ltac/coretactics.ml4 | 1 + plugins/ltac/extraargs.ml4 | 2 +- plugins/ltac/g_ltac.ml4 | 2 +- plugins/ltac/tacarg.ml | 8 ++++++ plugins/ltac/tacarg.mli | 26 ++++++++++++++++++- plugins/ltac/taccoerce.ml | 1 + plugins/ltac/tacexpr.ml | 2 +- plugins/ltac/tacexpr.mli | 2 +- proofs/tactypes.ml | 54 ++++++++++++++++++++++++++++++++++++++ 15 files changed, 109 insertions(+), 104 deletions(-) delete mode 100644 interp/tactypes.ml create mode 100644 proofs/tactypes.ml diff --git a/interp/genintern.ml b/interp/genintern.ml index 161201c44..d9a0db040 100644 --- a/interp/genintern.ml +++ b/interp/genintern.ml @@ -26,9 +26,15 @@ let empty_glob_sign env = { extra = Store.empty; } +(** In globalize tactics, we need to keep the initial [constr_expr] to recompute + in the environment by the effective calls to Intro, Inversion, etc + The [constr_expr] field is [None] in TacDef though *) +type glob_constr_and_expr = Glob_term.glob_constr * Constrexpr.constr_expr option +type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * Pattern.constr_pattern + type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb type 'glb subst_fun = substitution -> 'glb -> 'glb -type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb +type 'glb ntn_subst_fun = glob_constr_and_expr Id.Map.t -> 'glb -> 'glb module InternObj = struct diff --git a/interp/genintern.mli b/interp/genintern.mli index d818713fc..f4f064bca 100644 --- a/interp/genintern.mli +++ b/interp/genintern.mli @@ -22,6 +22,12 @@ type glob_sign = { val empty_glob_sign : Environ.env -> glob_sign +(** In globalize tactics, we need to keep the initial [constr_expr] to recompute + in the environment by the effective calls to Intro, Inversion, etc + The [constr_expr] field is [None] in TacDef though *) +type glob_constr_and_expr = Glob_term.glob_constr * Constrexpr.constr_expr option +type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * Pattern.constr_pattern + (** {5 Internalization functions} *) type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb @@ -42,7 +48,7 @@ val generic_substitute : glob_generic_argument subst_fun (** {5 Notation functions} *) -type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb +type 'glb ntn_subst_fun = glob_constr_and_expr Id.Map.t -> 'glb -> 'glb val substitute_notation : ('raw, 'glb, 'top) genarg_type -> 'glb ntn_subst_fun diff --git a/interp/stdarg.ml b/interp/stdarg.ml index e5ed58be6..7a7bb9a84 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -34,9 +34,6 @@ let wit_pre_ident : string uniform_genarg_type = let wit_int_or_var = make0 ~dyn:(val_tag (topwit wit_int)) "int_or_var" -let wit_intro_pattern = - make0 "intropattern" - let wit_ident = make0 "ident" @@ -45,8 +42,6 @@ let wit_var = let wit_ref = make0 "ref" -let wit_quant_hyp = make0 "quant_hyp" - let wit_sort_family = make0 "sort_family" let wit_constr = @@ -56,12 +51,6 @@ let wit_uconstr = make0 "uconstr" let wit_open_constr = make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr" -let wit_constr_with_bindings = make0 "constr_with_bindings" - -let wit_open_constr_with_bindings = make0 "open_constr_with_bindings" - -let wit_bindings = make0 "bindings" - let wit_red_expr = make0 "redexpr" let wit_clause_dft_concl = @@ -74,6 +63,4 @@ let wit_preident = wit_pre_ident let wit_reference = wit_ref let wit_global = wit_ref let wit_clause = wit_clause_dft_concl -let wit_quantified_hypothesis = wit_quant_hyp -let wit_intropattern = wit_intro_pattern let wit_redexpr = wit_red_expr diff --git a/interp/stdarg.mli b/interp/stdarg.mli index dc9c370a1..4159e6054 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -18,8 +18,8 @@ open Genredexpr open Pattern open Constrexpr open Misctypes -open Tactypes open Genarg +open Genintern val wit_unit : unit uniform_genarg_type @@ -35,16 +35,12 @@ val wit_pre_ident : string uniform_genarg_type val wit_int_or_var : (int or_var, int or_var, int) genarg_type -val wit_intro_pattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type - val wit_ident : Id.t uniform_genarg_type val wit_var : (lident, lident, Id.t) genarg_type val wit_ref : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type -val wit_quant_hyp : quantified_hypothesis uniform_genarg_type - val wit_sort_family : (Sorts.family, unit, unit) genarg_type val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type @@ -54,21 +50,6 @@ val wit_uconstr : (constr_expr , glob_constr_and_expr, Ltac_pretype.closed_glob_ val wit_open_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type -val wit_constr_with_bindings : - (constr_expr with_bindings, - glob_constr_and_expr with_bindings, - constr with_bindings delayed_open) genarg_type - -val wit_open_constr_with_bindings : - (constr_expr with_bindings, - glob_constr_and_expr with_bindings, - constr with_bindings delayed_open) genarg_type - -val wit_bindings : - (constr_expr bindings, - glob_constr_and_expr bindings, - constr bindings delayed_open) genarg_type - val wit_red_expr : ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, @@ -83,8 +64,6 @@ val wit_preident : string uniform_genarg_type val wit_reference : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type val wit_global : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type val wit_clause : (lident Locus.clause_expr, lident Locus.clause_expr, Names.Id.t Locus.clause_expr) genarg_type -val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type -val wit_intropattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type val wit_redexpr : ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, diff --git a/interp/tactypes.ml b/interp/tactypes.ml deleted file mode 100644 index f19abefee..000000000 --- a/interp/tactypes.ml +++ /dev/null @@ -1,62 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* Evd.evar_map -> Evd.evar_map * 'a - -type delayed_open_constr = EConstr.constr delayed_open -type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open - -type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t -type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list -type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t -type intro_pattern_naming = Namegen.intro_pattern_naming_expr CAst.t diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 24d1a40c2..9899b7b21 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -15,6 +15,7 @@ open Indfun_common open Indfun open Genarg open Stdarg +open Tacarg open Tactypes open Pcoq open Pcoq.Prim diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index 1070b30a1..8f59559eb 100644 --- a/plugins/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.ml4 @@ -15,6 +15,7 @@ open Tactypes open Genredexpr open Stdarg open Extraargs +open Tacarg open Names open Logic diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index 4e7c8b754..ddc157cac 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -35,7 +35,7 @@ let () = create_generic_quotation "ident" Pcoq.Prim.ident Stdarg.wit_ident let () = create_generic_quotation "reference" Pcoq.Prim.reference Stdarg.wit_ref let () = create_generic_quotation "uconstr" Pcoq.Constr.lconstr Stdarg.wit_uconstr let () = create_generic_quotation "constr" Pcoq.Constr.lconstr Stdarg.wit_constr -let () = create_generic_quotation "ipattern" Pltac.simple_intropattern Stdarg.wit_intro_pattern +let () = create_generic_quotation "ipattern" Pltac.simple_intropattern wit_intro_pattern let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Stdarg.wit_open_constr let () = let inject (loc, v) = Tacexpr.Tacexp v in diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index de9ff2875..c39192d46 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -36,7 +36,7 @@ let arg_of_expr = function let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) () let genarg_of_int n = in_gen (rawwit Stdarg.wit_int) n -let genarg_of_ipattern pat = in_gen (rawwit Stdarg.wit_intro_pattern) pat +let genarg_of_ipattern pat = in_gen (rawwit Tacarg.wit_intro_pattern) pat let genarg_of_uconstr c = in_gen (rawwit Stdarg.wit_uconstr) c let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac diff --git a/plugins/ltac/tacarg.ml b/plugins/ltac/tacarg.ml index 6eb482b1c..8a25d4851 100644 --- a/plugins/ltac/tacarg.ml +++ b/plugins/ltac/tacarg.ml @@ -19,6 +19,14 @@ let make0 ?dyn name = let () = Geninterp.register_val0 wit dyn in wit +let wit_intro_pattern = make0 "intropattern" +let wit_quant_hyp = make0 "quant_hyp" +let wit_constr_with_bindings = make0 "constr_with_bindings" +let wit_open_constr_with_bindings = make0 "open_constr_with_bindings" +let wit_bindings = make0 "bindings" +let wit_quantified_hypothesis = wit_quant_hyp +let wit_intropattern = wit_intro_pattern + let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type = make0 "tactic" diff --git a/plugins/ltac/tacarg.mli b/plugins/ltac/tacarg.mli index 1abe7cd6f..bdb0be03c 100644 --- a/plugins/ltac/tacarg.mli +++ b/plugins/ltac/tacarg.mli @@ -9,9 +9,33 @@ (************************************************************************) open Genarg -open Tacexpr +open EConstr open Constrexpr open Tactypes +open Tacexpr + +(** Tactic related witnesses, could also live in tactics/ if other users *) +val wit_intro_pattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type + +val wit_quant_hyp : quantified_hypothesis uniform_genarg_type + +val wit_constr_with_bindings : + (constr_expr with_bindings, + glob_constr_and_expr with_bindings, + constr with_bindings delayed_open) genarg_type + +val wit_open_constr_with_bindings : + (constr_expr with_bindings, + glob_constr_and_expr with_bindings, + constr with_bindings delayed_open) genarg_type + +val wit_bindings : + (constr_expr bindings, + glob_constr_and_expr bindings, + constr bindings delayed_open) genarg_type + +val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type +val wit_intropattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type (** Generic arguments based on Ltac. *) diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 27acbb629..6bfa07ee9 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -17,6 +17,7 @@ open Namegen open Tactypes open Genarg open Stdarg +open Tacarg open Geninterp open Pp diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 289434d8a..f4dd85bc2 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -118,7 +118,7 @@ type ml_tactic_entry = { (** Composite types *) -type glob_constr_and_expr = Tactypes.glob_constr_and_expr +type glob_constr_and_expr = Genintern.glob_constr_and_expr type open_constr_expr = unit * constr_expr type open_glob_constr = unit * glob_constr_and_expr diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 42f6883b4..be07654ef 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -118,7 +118,7 @@ type ml_tactic_entry = { (** Composite types *) -type glob_constr_and_expr = Tactypes.glob_constr_and_expr +type glob_constr_and_expr = Genintern.glob_constr_and_expr type open_constr_expr = unit * constr_expr type open_glob_constr = unit * glob_constr_and_expr diff --git a/proofs/tactypes.ml b/proofs/tactypes.ml new file mode 100644 index 000000000..86a7e9c52 --- /dev/null +++ b/proofs/tactypes.ml @@ -0,0 +1,54 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Evd.evar_map -> Evd.evar_map * 'a + +type delayed_open_constr = EConstr.constr delayed_open +type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open + +type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t +type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list +type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t +type intro_pattern_naming = Namegen.intro_pattern_naming_expr CAst.t -- cgit v1.2.3 From 4aaeb5d429227505adfde9fe04c3c0fb69f2d37f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 24 May 2018 04:38:30 +0200 Subject: [api] Misctypes removal: tactic flags. We move the "flag types" to its use place, and mark some arguments with named parameters better. --- pretyping/misctypes.ml | 9 --------- proofs/clenvtac.ml | 10 +++++----- proofs/clenvtac.mli | 7 +++---- tactics/auto.ml | 2 +- tactics/class_tactics.ml | 2 +- tactics/elim.mli | 3 +-- tactics/equality.ml | 4 ++-- tactics/equality.mli | 2 +- tactics/tacticals.ml | 10 +++++----- tactics/tacticals.mli | 3 +-- tactics/tactics.ml | 12 ++++++++---- tactics/tactics.mli | 6 +++++- 12 files changed, 33 insertions(+), 37 deletions(-) diff --git a/pretyping/misctypes.ml b/pretyping/misctypes.ml index c66c9b1b8..332a90182 100644 --- a/pretyping/misctypes.ml +++ b/pretyping/misctypes.ml @@ -26,12 +26,3 @@ type 'a or_by_notation = 'a or_by_notation_r CAst.t (* NB: the last string in [ByNotation] is actually a [Notation.delimiters], but this formulation avoids a useless dependency. *) - -(** Various flags *) - -type direction_flag = bool (* true = Left-to-right false = right-to-right *) -type evars_flag = bool (* true = pose evars false = fail on evars *) -type rec_flag = bool (* true = recursive false = not recursive *) -type advanced_flag = bool (* true = advanced false = basic *) -type letin_flag = bool (* true = use local def false = use Leibniz *) -type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 38ed63c23..544175c6d 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -54,7 +54,7 @@ let clenv_cast_meta clenv = let clenv_value_cast_meta clenv = clenv_cast_meta clenv (clenv_value clenv) -let clenv_pose_dependent_evars with_evars clenv = +let clenv_pose_dependent_evars ?(with_evars=false) clenv = let dep_mvs = clenv_dependent clenv in let env, sigma = clenv.env, clenv.evd in if not (List.is_empty dep_mvs) && not with_evars then @@ -75,12 +75,12 @@ let check_tc evd = let has_typeclass = Evar.Map.exists check (Evd.undefined_map evd) in (has_typeclass, !has_resolvable) -let clenv_refine with_evars ?(with_classes=true) clenv = +let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv = (** ppedrot: a Goal.enter here breaks things, because the tactic below may solve goals by side effects, while the compatibility layer keeps those useless goals. That deserves a FIXME. *) Proofview.V82.tactic begin fun gl -> - let clenv = clenv_pose_dependent_evars with_evars clenv in + let clenv = clenv_pose_dependent_evars ~with_evars clenv in let evd' = if with_classes then let (has_typeclass, has_resolvable) = check_tc clenv.evd in @@ -105,10 +105,10 @@ open Unification let dft = default_unify_flags -let res_pf ?(with_evars=false) ?(with_classes=true) ?(flags=dft ()) clenv = +let res_pf ?with_evars ?(with_classes=true) ?(flags=dft ()) clenv = Proofview.Goal.enter begin fun gl -> let clenv = clenv_unique_resolver ~flags clenv gl in - clenv_refine with_evars ~with_classes clenv + clenv_refine ?with_evars ~with_classes clenv end (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index 7c1e300b8..d17847842 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -13,12 +13,11 @@ open Clenv open EConstr open Unification -open Misctypes (** Tactics *) val unify : ?flags:unify_flags -> constr -> unit Proofview.tactic -val clenv_refine : evars_flag -> ?with_classes:bool -> clausenv -> unit Proofview.tactic -val res_pf : ?with_evars:evars_flag -> ?with_classes:bool -> ?flags:unify_flags -> clausenv -> unit Proofview.tactic +val clenv_refine : ?with_evars:bool -> ?with_classes:bool -> clausenv -> unit Proofview.tactic +val res_pf : ?with_evars:bool -> ?with_classes:bool -> ?flags:unify_flags -> clausenv -> unit Proofview.tactic -val clenv_pose_dependent_evars : evars_flag -> clausenv -> clausenv +val clenv_pose_dependent_evars : ?with_evars:bool -> clausenv -> clausenv val clenv_value_cast_meta : clausenv -> constr diff --git a/tactics/auto.ml b/tactics/auto.ml index 77fe31415..d7de6c4fb 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -99,7 +99,7 @@ let unify_resolve poly flags ((c : raw_hint), clenv) = Proofview.Goal.enter begin fun gl -> let clenv, c = connect_hint_clenv poly c clenv gl in let clenv = clenv_unique_resolver ~flags clenv gl in - Clenvtac.clenv_refine false clenv + Clenvtac.clenv_refine clenv end let unify_resolve_nodelta poly h = unify_resolve poly auto_unif_flags h diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 4beeaaae0..773fc1520 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -207,7 +207,7 @@ let clenv_unique_resolver_tac with_evars ~flags clenv' = try Proofview.tclUNIT (clenv_unique_resolver ~flags clenv' gls) with e -> Proofview.tclZERO e in resolve >>= fun clenv' -> - Clenvtac.clenv_refine with_evars ~with_classes:false clenv' + Clenvtac.clenv_refine ~with_evars ~with_classes:false clenv' end let unify_e_resolve poly flags = begin fun gls (c,_,clenv) -> diff --git a/tactics/elim.mli b/tactics/elim.mli index d6b67e5ba..ddfac3f2c 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -11,12 +11,11 @@ open Names open EConstr open Tacticals -open Misctypes open Tactypes (** Eliminations tactics. *) -val introCaseAssumsThen : evars_flag -> +val introCaseAssumsThen : Tactics.evars_flag -> (intro_patterns -> branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic diff --git a/tactics/equality.ml b/tactics/equality.ml index 1033c56c9..671e765e0 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -155,7 +155,7 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl = let c1 = args.(arglen - 2) in let c2 = args.(arglen - 1) in let try_occ (evd', c') = - Clenvtac.clenv_pose_dependent_evars true {eqclause with evd = evd'} + Clenvtac.clenv_pose_dependent_evars ~with_evars:true {eqclause with evd = evd'} in let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in let occs = @@ -1044,7 +1044,7 @@ let onEquality with_evars tac (c,lbindc) = let t = type_of c in let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in - let eq_clause' = Clenvtac.clenv_pose_dependent_evars with_evars eq_clause in + let eq_clause' = Clenvtac.clenv_pose_dependent_evars ~with_evars eq_clause in let eqn = clenv_type eq_clause' in let (eq,u,eq_args) = find_this_eq_data_decompose gl eqn in tclTHEN diff --git a/tactics/equality.mli b/tactics/equality.mli index 9395cf4a8..6f3e08ea0 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -15,8 +15,8 @@ open EConstr open Environ open Ind_tables open Locus -open Misctypes open Tactypes +open Tactics (*i*) type dep_proof_flag = bool (* true = support rewriting dependent proofs *) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 53a02f89b..f34c83ae7 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -223,7 +223,7 @@ let compute_induction_names_gen check_and branchletsigns = function let compute_induction_names = compute_induction_names_gen true (* Compute the let-in signature of case analysis or standard induction scheme *) -let compute_constructor_signatures isrec ((_,k as ity),u) = +let compute_constructor_signatures ~rec_flag ((_,k as ity),u) = let rec analrec c recargs = match Constr.kind c, recargs with | Prod (_,_,c), recarg::rest -> @@ -231,7 +231,7 @@ let compute_constructor_signatures isrec ((_,k as ity),u) = begin match Declareops.dest_recarg recarg with | Norec | Imbr _ -> true :: rest | Mrec (_,j) -> - if isrec && Int.equal j k then true :: true :: rest + if rec_flag && Int.equal j k then true :: true :: rest else true :: rest end | LetIn (_,_,_,c), rest -> false :: analrec c rest @@ -634,7 +634,7 @@ module New = struct (* Find the right elimination suffix corresponding to the sort of the goal *) (* c should be of type A1->.. An->B with B an inductive definition *) let general_elim_then_using mk_elim - isrec allnames tac predicate ind (c, t) = + rec_flag allnames tac predicate ind (c, t) = Proofview.Goal.enter begin fun gl -> let sigma, elim = mk_elim ind gl in let ind = on_snd (fun u -> EInstance.kind sigma u) ind in @@ -663,7 +663,7 @@ module New = struct (str "The elimination combinator " ++ str name_elim ++ str " is unknown.") in let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in - let branchsigns = compute_constructor_signatures isrec ind in + let branchsigns = compute_constructor_signatures ~rec_flag ind in let brnames = compute_induction_names_gen false branchsigns allnames in let flags = Unification.elim_flags () in let elimclause' = @@ -686,7 +686,7 @@ module New = struct in let branchtacs = List.init (Array.length branchsigns) after_tac in Proofview.tclTHEN - (Clenvtac.clenv_refine false clenv') + (Clenvtac.clenv_refine clenv') (Proofview.tclEXTEND [] tclIDTAC branchtacs) end) end diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index cbaf691f1..1e66c2b0b 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -14,7 +14,6 @@ open EConstr open Evd open Proof_type open Locus -open Misctypes open Tactypes (** Tacticals i.e. functions from tactics to tactics. *) @@ -124,7 +123,7 @@ val fix_empty_or_and_pattern : int -> delayed_open_constr or_and_intro_pattern_expr -> delayed_open_constr or_and_intro_pattern_expr -val compute_constructor_signatures : rec_flag -> inductive * 'a -> bool list array +val compute_constructor_signatures : rec_flag:bool -> inductive * 'a -> bool list array (** Useful for [as intro_pattern] modifier *) val compute_induction_names : diff --git a/tactics/tactics.ml b/tactics/tactics.ml index cf07532c0..67170d2cf 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -43,7 +43,6 @@ open Pretype_errors open Unification open Locus open Locusops -open Misctypes open Tactypes open Proofview.Notations open Context.Named.Declaration @@ -1154,6 +1153,11 @@ let tactic_infer_flags with_evar = { Pretyping.fail_evar = not with_evar; Pretyping.expand_evars = true } +type evars_flag = bool (* true = pose evars false = fail on evars *) +type rec_flag = bool (* true = recursive false = not recursive *) +type advanced_flag = bool (* true = advanced false = basic *) +type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) + type 'a core_destruction_arg = | ElimOnConstr of 'a | ElimOnIdent of lident @@ -1282,7 +1286,7 @@ let do_replace id = function let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) targetid id sigma0 clenv tac = - let clenv = Clenvtac.clenv_pose_dependent_evars with_evars clenv in + let clenv = Clenvtac.clenv_pose_dependent_evars ~with_evars clenv in let clenv = if with_classes then { clenv with evd = Typeclasses.resolve_typeclasses @@ -2259,7 +2263,7 @@ let intro_or_and_pattern ?loc with_evars bracketed ll thin tac id = let c = mkVar id in let t = Tacmach.New.pf_unsafe_type_of gl c in let (ind,t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in - let branchsigns = compute_constructor_signatures false ind in + let branchsigns = compute_constructor_signatures ~rec_flag:false ind in let nv_with_let = Array.map List.length branchsigns in let ll = fix_empty_or_and_pattern (Array.length branchsigns) ll in let ll = get_and_check_or_and_pattern ?loc ll branchsigns in @@ -4197,7 +4201,7 @@ let induction_tac with_evars params indvars elim = let elimclause' = recolle_clenv i params indvars elimclause gl in (* one last resolution (useless?) *) let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in - Clenvtac.clenv_refine with_evars resolved + Clenvtac.clenv_refine ~with_evars resolved end (* Apply induction "in place" taking into account dependent diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 086442e42..8d4302450 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -18,7 +18,6 @@ open Clenv open Redexpr open Pattern open Unification -open Misctypes open Tactypes open Locus open Ltac_pretype @@ -91,6 +90,11 @@ val intros_clearing : bool list -> unit Proofview.tactic val try_intros_until : (Id.t -> unit Proofview.tactic) -> quantified_hypothesis -> unit Proofview.tactic +type evars_flag = bool (* true = pose evars false = fail on evars *) +type rec_flag = bool (* true = recursive false = not recursive *) +type advanced_flag = bool (* true = advanced false = basic *) +type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) + (** Apply a tactic on a quantified hypothesis, an hypothesis in context or a term with bindings *) -- cgit v1.2.3 From 615290d0f9d5cad7c508d45cf4ab89aecff033b2 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 1 Jun 2018 02:37:15 +0200 Subject: [api] Remove Misctypes. We move the last 3 types to more adequate places. --- interp/constrexpr.ml | 9 +++++++++ interp/genredexpr.ml | 1 - interp/smartlocate.ml | 5 ++--- interp/smartlocate.mli | 5 ++--- interp/stdarg.ml | 2 ++ interp/stdarg.mli | 4 +++- library/library.mllib | 1 - parsing/g_prim.ml4 | 4 ++-- parsing/pcoq.mli | 1 - plugins/extraction/extract_env.ml | 2 +- plugins/ltac/coretactics.ml4 | 1 - plugins/ltac/extraargs.ml4 | 1 - plugins/ltac/extraargs.mli | 7 +++---- plugins/ltac/g_ltac.ml4 | 7 +++---- plugins/ltac/g_tactic.ml4 | 1 - plugins/ltac/pltac.mli | 3 +-- plugins/ltac/pptactic.ml | 1 - plugins/ltac/pptactic.mli | 3 +-- plugins/ltac/taccoerce.ml | 3 +-- plugins/ltac/taccoerce.mli | 3 +-- plugins/ltac/tacentries.ml | 2 +- plugins/ltac/tacexpr.ml | 3 +-- plugins/ltac/tacexpr.mli | 3 +-- plugins/ltac/tacintern.ml | 1 - plugins/ltac/tacinterp.ml | 1 - plugins/ltac/tacinterp.mli | 3 +-- plugins/ltac/tacsubst.ml | 3 +-- plugins/ltac/tauto.ml | 5 ++--- plugins/quote/g_quote.ml4 | 3 +-- plugins/setoid_ring/newring.ml | 2 +- plugins/ssr/ssrast.mli | 2 +- plugins/ssr/ssrcommon.ml | 1 - plugins/ssr/ssrparser.ml4 | 16 ++++++++-------- plugins/ssr/ssrtacticals.ml | 3 +-- plugins/ssr/ssrtacticals.mli | 4 ++-- plugins/ssr/ssrvernac.ml4 | 1 - pretyping/locus.ml | 5 ++++- pretyping/locusops.ml | 4 ++-- pretyping/misctypes.ml | 28 ---------------------------- printing/ppconstr.ml | 5 ++--- printing/ppconstr.mli | 3 +-- printing/pputils.ml | 3 +-- printing/pputils.mli | 3 +-- printing/prettyp.ml | 9 ++++----- printing/prettyp.mli | 7 +++---- proofs/redexpr.ml | 5 ++--- tactics/equality.ml | 1 - vernac/g_vernac.ml4 | 1 - vernac/vernacentries.ml | 3 +-- vernac/vernacentries.mli | 4 +--- vernac/vernacexpr.ml | 1 - 51 files changed, 74 insertions(+), 125 deletions(-) delete mode 100644 pretyping/misctypes.ml diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index 60f2c683a..d725f5afa 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -22,6 +22,15 @@ type name_decl = lname * universe_decl_expr option type notation = string +type 'a or_by_notation_r = + | AN of 'a + | ByNotation of (string * string option) + +type 'a or_by_notation = 'a or_by_notation_r CAst.t + +(* NB: the last string in [ByNotation] is actually a [Notation.delimiters], + but this formulation avoids a useless dependency. *) + type explicitation = | ExplByPos of int * Id.t option (* a reference to the n-th product starting from left *) | ExplByName of Id.t diff --git a/interp/genredexpr.ml b/interp/genredexpr.ml index 983493b25..42c1fe429 100644 --- a/interp/genredexpr.ml +++ b/interp/genredexpr.ml @@ -57,7 +57,6 @@ type ('a,'b,'c) may_eval = open Libnames open Constrexpr -open Misctypes type r_trm = constr_expr type r_pat = constr_pattern_expr diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index 1f4a93a6f..e1fbdba87 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -18,7 +18,6 @@ open Pp open CErrors open Libnames open Globnames -open Misctypes open Syntax_def open Notation_term @@ -65,13 +64,13 @@ let global_with_alias ?head r = try locate_global_with_alias ?head qid with Not_found -> Nametab.error_global_not_found qid -let smart_global ?head = CAst.with_loc_val (fun ?loc -> function +let smart_global ?head = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function | AN r -> global_with_alias ?head r | ByNotation (ntn,sc) -> Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc) -let smart_global_inductive = CAst.with_loc_val (fun ?loc -> function +let smart_global_inductive = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function | AN r -> global_inductive_with_alias r | ByNotation (ntn,sc) -> diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli index 45037b8b3..6b574d7b5 100644 --- a/interp/smartlocate.mli +++ b/interp/smartlocate.mli @@ -11,7 +11,6 @@ open Names open Libnames open Globnames -open Misctypes (** [locate_global_with_alias] locates global reference possibly following a notation if this notation has a role of aliasing; raise [Not_found] @@ -33,7 +32,7 @@ val global_with_alias : ?head:bool -> reference -> GlobRef.t val global_inductive_with_alias : reference -> inductive (** Locate a reference taking into account notations and "aliases" *) -val smart_global : ?head:bool -> reference or_by_notation -> GlobRef.t +val smart_global : ?head:bool -> reference Constrexpr.or_by_notation -> GlobRef.t (** The same for inductive types *) -val smart_global_inductive : reference or_by_notation -> inductive +val smart_global_inductive : reference Constrexpr.or_by_notation -> inductive diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 7a7bb9a84..7b01b6dc1 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -11,6 +11,8 @@ open Genarg open Geninterp +type 'a and_short_name = 'a * Names.lident option + let make0 ?dyn name = let wit = Genarg.make0 name in let () = register_val0 wit dyn in diff --git a/interp/stdarg.mli b/interp/stdarg.mli index 4159e6054..4792cda08 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -17,9 +17,11 @@ open Libnames open Genredexpr open Pattern open Constrexpr -open Misctypes open Genarg open Genintern +open Locus + +type 'a and_short_name = 'a * lident option val wit_unit : unit uniform_genarg_type diff --git a/library/library.mllib b/library/library.mllib index 1c0368847..2ac4266fc 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -6,7 +6,6 @@ Nametab Global Decl_kinds Lib -Misctypes Declaremods Loadpath Library diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index b25ea766a..08bcd0f8c 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -85,8 +85,8 @@ GEXTEND Gram [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> (s, sc) ] ] ; smart_global: - [ [ c = reference -> CAst.make ~loc:!@loc @@ Misctypes.AN c - | ntn = by_notation -> CAst.make ~loc:!@loc @@ Misctypes.ByNotation ntn ] ] + [ [ c = reference -> CAst.make ~loc:!@loc @@ Constrexpr.AN c + | ntn = by_notation -> CAst.make ~loc:!@loc @@ Constrexpr.ByNotation ntn ] ] ; qualid: [ [ qid = basequalid -> CAst.make ~loc:!@loc qid ] ] diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 00ca53884..9a45bc973 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -13,7 +13,6 @@ open Extend open Genarg open Constrexpr open Libnames -open Misctypes (** The parser of Coq *) diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index bebd27e11..1e0589fac 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -646,7 +646,7 @@ let separate_extraction lr = is \verb!Extraction! [qualid]. *) let simple_extraction r = - Vernacentries.dump_global CAst.(make (Misctypes.AN r)); + Vernacentries.dump_global CAst.(make (Constrexpr.AN r)); match locate_ref [r] with | ([], [mp]) as p -> full_extr None p | [r],[] -> diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index 8f59559eb..61525cb49 100644 --- a/plugins/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.ml4 @@ -10,7 +10,6 @@ open Util open Locus -open Misctypes open Tactypes open Genredexpr open Stdarg diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index ddc157cac..dae2582bd 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -19,7 +19,6 @@ open Tacmach open Tacexpr open Taccoerce open Tacinterp -open Misctypes open Locus (** Adding scopes for generic arguments not defined through ARGUMENT EXTEND *) diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index ff697e3c7..737147884 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -12,7 +12,6 @@ open Tacexpr open Names open Constrexpr open Glob_term -open Misctypes val wit_orient : bool Genarg.uniform_genarg_type val orient : bool Pcoq.Gram.entry @@ -20,9 +19,9 @@ val pr_orient : bool -> Pp.t val wit_rename : (Id.t * Id.t) Genarg.uniform_genarg_type -val occurrences : (int list or_var) Pcoq.Gram.entry -val wit_occurrences : (int list or_var, int list or_var, int list) Genarg.genarg_type -val pr_occurrences : int list or_var -> Pp.t +val occurrences : (int list Locus.or_var) Pcoq.Gram.entry +val wit_occurrences : (int list Locus.or_var, int list Locus.or_var, int list) Genarg.genarg_type +val pr_occurrences : int list Locus.or_var -> Pp.t val occurrences_of : int list -> Locus.occurrences val wit_natural : int Genarg.uniform_genarg_type diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index c39192d46..d7d642e50 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -15,7 +15,6 @@ open Pp open Glob_term open Constrexpr open Tacexpr -open Misctypes open Namegen open Genarg open Genredexpr @@ -28,7 +27,7 @@ open Pcoq.Constr open Pvernac.Vernac_ open Pltac -let fail_default_value = ArgArg 0 +let fail_default_value = Locus.ArgArg 0 let arg_of_expr = function TacArg (loc,a) -> a @@ -199,9 +198,9 @@ GEXTEND Gram non ambiguous name where dots are replaced by "_"? Probably too verbose most of the time. *) fresh_id: - [ [ s = STRING -> ArgArg s (*| id = ident -> ArgVar (!@loc,id)*) + [ [ s = STRING -> Locus.ArgArg s (*| id = ident -> Locus.ArgVar (!@loc,id)*) | qid = qualid -> let (_pth,id) = Libnames.repr_qualid qid.CAst.v in - ArgVar (CAst.make ~loc:!@loc id) ] ] + Locus.ArgVar (CAst.make ~loc:!@loc id) ] ] ; constr_eval: [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index c91c160f0..05005c733 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -18,7 +18,6 @@ open Genredexpr open Constrexpr open Libnames open Tok -open Misctypes open Tactypes open Locus open Decl_kinds diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index a75ca8ecb..4c075d413 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -15,7 +15,6 @@ open Libnames open Constrexpr open Tacexpr open Genredexpr -open Misctypes open Tactypes val open_constr : constr_expr Gram.entry @@ -27,7 +26,7 @@ val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gr val uconstr : constr_expr Gram.entry val quantified_hypothesis : quantified_hypothesis Gram.entry val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Gram.entry -val int_or_var : int or_var Gram.entry +val int_or_var : int Locus.or_var Gram.entry val simple_tactic : raw_tactic_expr Gram.entry val simple_intropattern : constr_expr intro_pattern_expr CAst.t Gram.entry val in_clause : Names.lident Locus.clause_expr Gram.entry diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 7b72a4bf9..e19a95e84 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -19,7 +19,6 @@ open Geninterp open Stdarg open Libnames open Notation_gram -open Misctypes open Tactypes open Locus open Decl_kinds diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index c14874d6c..6c09e447a 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -14,7 +14,6 @@ open Genarg open Geninterp open Names -open Misctypes open Environ open Constrexpr open Notation_gram @@ -98,7 +97,7 @@ val pr_may_eval : ('a -> Pp.t) -> ('a -> Pp.t) -> ('b -> Pp.t) -> ('c -> Pp.t) -> ('a,'b,'c) Genredexpr.may_eval -> Pp.t -val pr_and_short_name : ('a -> Pp.t) -> 'a and_short_name -> Pp.t +val pr_and_short_name : ('a -> Pp.t) -> 'a Stdarg.and_short_name -> Pp.t val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t val pr_evaluable_reference_env : env -> evaluable_global_reference -> Pp.t diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 6bfa07ee9..cc9c2046d 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -12,7 +12,6 @@ open Util open Names open Constr open EConstr -open Misctypes open Namegen open Tactypes open Genarg @@ -368,7 +367,7 @@ let coerce_to_int_or_var_list v = match Value.to_list v with | None -> raise (CannotCoerceTo "an int list") | Some l -> - let map n = ArgArg (coerce_to_int n) in + let map n = Locus.ArgArg (coerce_to_int n) in List.map map l (** Abstract application, to print ltac functions *) diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index 31bce197b..56f881684 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -11,7 +11,6 @@ open Util open Names open EConstr -open Misctypes open Genarg open Geninterp open Tactypes @@ -87,7 +86,7 @@ val coerce_to_quantified_hypothesis : Evd.evar_map -> Value.t -> quantified_hypo val coerce_to_decl_or_quant_hyp : Environ.env -> Evd.evar_map -> Value.t -> quantified_hypothesis -val coerce_to_int_or_var_list : Value.t -> int or_var list +val coerce_to_int_or_var_list : Value.t -> int Locus.or_var list (** {5 Missing generic arguments} *) diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index e510b9f59..fada7424c 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -376,7 +376,7 @@ let add_ml_tactic_notation name ~level prods = in let ids = List.map_filter get_id prods in let entry = { mltac_name = name; mltac_index = len - i - 1 } in - let map id = Reference (Misctypes.ArgVar (CAst.make id)) in + let map id = Reference (Locus.ArgVar (CAst.make id)) in let tac = TacML (Loc.tag (entry, List.map map ids)) in add_glob_tactic_notation false ~level prods true ids tac in diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index f4dd85bc2..d51de8c65 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -15,7 +15,6 @@ open Libnames open Genredexpr open Genarg open Pattern -open Misctypes open Tactypes open Locus @@ -306,7 +305,7 @@ constraint 'a = < type g_trm = glob_constr_and_expr type g_pat = glob_constr_pattern_and_expr -type g_cst = evaluable_global_reference and_short_name or_var +type g_cst = evaluable_global_reference Stdarg.and_short_name or_var type g_ref = ltac_constant located or_var type g_nam = lident diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index be07654ef..01eead164 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -15,7 +15,6 @@ open Libnames open Genredexpr open Genarg open Pattern -open Misctypes open Locus open Tactypes @@ -306,7 +305,7 @@ constraint 'a = < type g_trm = glob_constr_and_expr type g_pat = glob_constr_pattern_and_expr -type g_cst = evaluable_global_reference and_short_name or_var +type g_cst = evaluable_global_reference Stdarg.and_short_name or_var type g_ref = ltac_constant located or_var type g_nam = lident diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 2a5c38024..cef5bb1b8 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -27,7 +27,6 @@ open Tacexpr open Genarg open Stdarg open Tacarg -open Misctypes open Namegen open Tactypes open Locus diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 04c93eae3..8a8f9e71a 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -36,7 +36,6 @@ open Stdarg open Tacarg open Printer open Pretyping -open Misctypes open Tactypes open Locus open Tacintern diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index e18f6ab19..fd2d96bd6 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -14,7 +14,6 @@ open EConstr open Tacexpr open Genarg open Redexpr -open Misctypes open Tactypes val ltac_trace_info : ltac_trace Exninfo.t @@ -132,7 +131,7 @@ val interp_ltac_var : (value -> 'a) -> interp_sign -> val interp_int : interp_sign -> lident -> int -val interp_int_or_var : interp_sign -> int or_var -> int +val interp_int_or_var : interp_sign -> int Locus.or_var -> int val default_ist : unit -> Geninterp.interp_sign (** Empty ist with debug set on the current value. *) diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 0b86a68b0..dd799dc13 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -14,7 +14,6 @@ open Mod_subst open Genarg open Stdarg open Tacarg -open Misctypes open Tactypes open Globnames open Genredexpr @@ -76,7 +75,7 @@ let subst_and_short_name f (c,n) = (* assert (n=None); *)(* since tacdef are strictly globalized *) (f c,None) -let subst_or_var f = function +let subst_or_var f = let open Locus in function | ArgVar _ as x -> x | ArgArg x -> ArgArg (f x) diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 368c20469..299bc7ea4 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -13,7 +13,6 @@ open EConstr open Hipattern open Names open Geninterp -open Misctypes open Ltac_plugin open Tacexpr open Tacinterp @@ -187,7 +186,7 @@ let flatten_contravariant_disj _ ist = let make_unfold name = let dir = DirPath.make (List.map Id.of_string ["Logic"; "Init"; "Coq"]) in let const = Constant.make2 (ModPath.MPfile dir) (Label.make name) in - (Locus.AllOccurrences, ArgArg (EvalConstRef const, None)) + Locus.(AllOccurrences, ArgArg (EvalConstRef const, None)) let u_not = make_unfold "not" @@ -245,7 +244,7 @@ let with_flags flags _ ist = let x = CAst.make @@ Id.of_string "x" in let arg = Val.Dyn (tag_tauto_flags, flags) in let ist = { ist with lfun = Id.Map.add x.CAst.v arg ist.lfun } in - eval_tactic_ist ist (TacArg (Loc.tag @@ TacCall (Loc.tag (ArgVar f, [Reference (ArgVar x)])))) + eval_tactic_ist ist (TacArg (Loc.tag @@ TacCall (Loc.tag (Locus.ArgVar f, [Reference (Locus.ArgVar x)])))) let register_tauto_tactic tac name0 args = let ids = List.map (fun id -> Id.of_string id) args in diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index c35e0fe12..09209dc22 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -10,7 +10,6 @@ open Ltac_plugin open Names -open Misctypes open Tacexpr open Geninterp open Quote @@ -24,7 +23,7 @@ let x = Id.of_string "x" let make_cont (k : Val.t) (c : EConstr.t) = let c = Tacinterp.Value.of_constr c in - let tac = TacCall (Loc.tag (ArgVar CAst.(make cont), [Reference (ArgVar CAst.(make x))])) in + let tac = TacCall (Loc.tag (Locus.ArgVar CAst.(make cont), [Reference (Locus.ArgVar CAst.(make x))])) in let ist = { lfun = Id.Map.add cont k (Id.Map.singleton x c); extra = TacStore.empty; } in Tacinterp.eval_tactic_ist ist (TacArg (Loc.tag tac)) diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index b9d0d2e25..84b29a0bf 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -20,6 +20,7 @@ open Environ open Libnames open Globnames open Glob_term +open Locus open Tacexpr open Coqlib open Mod_subst @@ -29,7 +30,6 @@ open Printer open Declare open Decl_kinds open Entries -open Misctypes open Newring_ast open Proofview.Notations diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index 7f5f2f63d..5571c5420 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -37,7 +37,7 @@ type ssrmult = int * ssrmmod type ssrocc = (bool * int list) option (* index MAYBE REMOVE ONLY INTERNAL stuff between {} *) -type ssrindex = int Misctypes.or_var +type ssrindex = int Locus.or_var (* clear switch {H G} *) type ssrclear = ssrhyps diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index ea7216832..2a31157be 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -181,7 +181,6 @@ let option_assert_get o msg = (** Constructors for rawconstr *) open Glob_term open Globnames -open Misctypes open Decl_kinds let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 9d7fc254c..352f88bb3 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -22,13 +22,13 @@ open Libnames open Tactics open Tacmach open Util +open Locus open Tacexpr open Tacinterp open Pltac open Extraargs open Ppconstr -open Misctypes open Namegen open Tactypes open Decl_kinds @@ -303,24 +303,24 @@ END let pr_index = function - | Misctypes.ArgVar {CAst.v=id} -> pr_id id - | Misctypes.ArgArg n when n > 0 -> int n + | ArgVar {CAst.v=id} -> pr_id id + | ArgArg n when n > 0 -> int n | _ -> mt () let pr_ssrindex _ _ _ = pr_index -let noindex = Misctypes.ArgArg 0 +let noindex = ArgArg 0 let check_index ?loc i = if i > 0 then i else CErrors.user_err ?loc (str"Index not positive") let mk_index ?loc = function - | Misctypes.ArgArg i -> Misctypes.ArgArg (check_index ?loc i) + | ArgArg i -> ArgArg (check_index ?loc i) | iv -> iv let interp_index ist gl idx = Tacmach.project gl, match idx with - | Misctypes.ArgArg _ -> idx - | Misctypes.ArgVar id -> + | ArgArg _ -> idx + | ArgVar id -> let i = try let v = Id.Map.find id.CAst.v ist.Tacinterp.lfun in @@ -338,7 +338,7 @@ let interp_index ist gl idx = | None -> raise Not_found end end with _ -> CErrors.user_err ?loc:id.CAst.loc (str"Index not a number") in - Misctypes.ArgArg (check_index ?loc:id.CAst.loc i) + ArgArg (check_index ?loc:id.CAst.loc i) open Pltac diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index 372ae86bd..83581f341 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -14,7 +14,6 @@ open Names open Constr open Termops open Tacmach -open Misctypes open Locusops open Ssrast @@ -25,7 +24,7 @@ module NamedDecl = Context.Named.Declaration (** Tacticals (+, -, *, done, by, do, =>, first, and last). *) -let get_index = function ArgArg i -> i | _ -> +let get_index = function Locus.ArgArg i -> i | _ -> anomaly "Uninterpreted index" (* Toplevel constr must be globalized twice ! *) diff --git a/plugins/ssr/ssrtacticals.mli b/plugins/ssr/ssrtacticals.mli index a5636ad0f..684e00235 100644 --- a/plugins/ssr/ssrtacticals.mli +++ b/plugins/ssr/ssrtacticals.mli @@ -17,7 +17,7 @@ val tclSEQAT : Tacinterp.interp_sign -> Tacinterp.Value.t -> Ssrast.ssrdir -> - int Misctypes.or_var * + int Locus.or_var * (('a * Tacinterp.Value.t option list) * Tacinterp.Value.t option) -> Tacmach.tactic @@ -37,7 +37,7 @@ val hinttac : val ssrdotac : Tacinterp.interp_sign -> - ((int Misctypes.or_var * Ssrast.ssrmmod) * + ((int Locus.or_var * Ssrast.ssrmmod) * (bool * Tacinterp.Value.t option list)) * ((Ssrast.ssrhyps * ((Ssrast.ssrhyp_or_id * string) * diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 750461a1b..939e97866 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -27,7 +27,6 @@ open Glob_term open Globnames open Stdarg open Genarg -open Misctypes open Decl_kinds open Libnames open Pp diff --git a/pretyping/locus.ml b/pretyping/locus.ml index 95a2e495b..37dd120c1 100644 --- a/pretyping/locus.ml +++ b/pretyping/locus.ml @@ -9,10 +9,13 @@ (************************************************************************) open Names -open Misctypes (** Locus : positions in hypotheses and goals *) +type 'a or_var = + | ArgArg of 'a + | ArgVar of lident + (** {6 Occurrences} *) type 'a occurrences_gen = diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index 1664e68f2..6b6a3f8a9 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -86,8 +86,8 @@ let concrete_clause_of enum_hyps cl = (** Miscellaneous functions *) let out_arg = function - | Misctypes.ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable.") - | Misctypes.ArgArg x -> x + | ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable.") + | ArgArg x -> x let occurrences_of_hyp id cls = let rec hyp_occ = function diff --git a/pretyping/misctypes.ml b/pretyping/misctypes.ml deleted file mode 100644 index 332a90182..000000000 --- a/pretyping/misctypes.ml +++ /dev/null @@ -1,28 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* Pp.t) -> 'a or_var -> Pp.t +val pr_or_var : ('a -> Pp.t) -> 'a Locus.or_var -> Pp.t val pr_lident : lident -> Pp.t val pr_lname : lname -> Pp.t diff --git a/printing/pputils.ml b/printing/pputils.ml index c14aa318e..c6b8d5022 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -11,7 +11,6 @@ open Util open Pp open Genarg -open Misctypes open Locus open Genredexpr @@ -122,7 +121,7 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) keyword = function let pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_ref,pr_pattern) = pr_red_expr (pr_constr env sigma, pr_lconstr env sigma, pr_ref, pr_pattern env sigma) -let pr_or_by_notation f = function +let pr_or_by_notation f = let open Constrexpr in function | {CAst.loc; v=AN v} -> f v | {CAst.loc; v=ByNotation (s,sc)} -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc diff --git a/printing/pputils.mli b/printing/pputils.mli index 6039168f8..5b1969e23 100644 --- a/printing/pputils.mli +++ b/printing/pputils.mli @@ -9,7 +9,6 @@ (************************************************************************) open Genarg -open Misctypes open Locus open Genredexpr @@ -18,7 +17,7 @@ val pr_ast : ('a -> Pp.t) -> 'a CAst.t -> Pp.t (** Prints an object surrounded by its commented location *) val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t -val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t +val pr_or_by_notation : ('a -> Pp.t) -> 'a Constrexpr.or_by_notation -> Pp.t val pr_with_occurrences : ('a -> Pp.t) -> (string -> Pp.t) -> 'a with_occurrences -> Pp.t diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 895181bc5..fe6cf73c7 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -26,7 +26,6 @@ open Libobject open Libnames open Globnames open Recordops -open Misctypes open Printer open Printmod open Context.Rel.Declaration @@ -843,12 +842,12 @@ let print_any_name env sigma na udecl = let print_name env sigma na udecl = match na with - | {loc; v=ByNotation (ntn,sc)} -> + | {loc; v=Constrexpr.ByNotation (ntn,sc)} -> print_any_name env sigma (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) udecl - | {loc; v=AN ref} -> + | {loc; v=Constrexpr.AN ref} -> print_any_name env sigma (locate_any_name ref) udecl let print_opaque_name env sigma qid = @@ -896,11 +895,11 @@ let print_about_any ?loc env sigma k udecl = let print_about env sigma na udecl = match na with - | {loc;v=ByNotation (ntn,sc)} -> + | {loc;v=Constrexpr.ByNotation (ntn,sc)} -> print_about_any ?loc env sigma (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) udecl - | {loc;v=AN ref} -> + | {loc;v=Constrexpr.AN ref} -> print_about_any ?loc env sigma (locate_any_name ref) udecl (* for debug *) diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 50042d6c5..0375cfc92 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -12,7 +12,6 @@ open Names open Environ open Reductionops open Libnames -open Misctypes open Evd (** A Pretty-Printer for the Calculus of Inductive Constructions. *) @@ -33,12 +32,12 @@ val print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t -val print_name : env -> Evd.evar_map -> reference or_by_notation -> +val print_name : env -> Evd.evar_map -> reference Constrexpr.or_by_notation -> UnivNames.univ_name_list option -> Pp.t val print_opaque_name : env -> Evd.evar_map -> reference -> Pp.t -val print_about : env -> Evd.evar_map -> reference or_by_notation -> +val print_about : env -> Evd.evar_map -> reference Constrexpr.or_by_notation -> UnivNames.univ_name_list option -> Pp.t -val print_impargs : reference or_by_notation -> Pp.t +val print_impargs : reference Constrexpr.or_by_notation -> Pp.t (** Pretty-printing functions for classes and coercions *) val print_graph : env -> evar_map -> Pp.t diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 03ebc3275..629b77be2 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -23,7 +23,6 @@ open Tacred open CClosure open RedFlags open Libobject -open Misctypes (* call by value normalisation function using the virtual machine *) let cbv_vm env sigma c = @@ -200,8 +199,8 @@ let decl_red_expr s e = end let out_arg = function - | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.") - | ArgArg x -> x + | Locus.ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.") + | Locus.ArgArg x -> x let out_with_occurrences (occs,c) = (Locusops.occurrences_map (List.map out_arg) occs, c) diff --git a/tactics/equality.ml b/tactics/equality.ml index 671e765e0..91c577405 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -42,7 +42,6 @@ open Ind_tables open Eqschemes open Locus open Locusops -open Misctypes open Tactypes open Proofview.Notations open Unification diff --git a/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4 index 59449d07a..3a59242de 100644 --- a/vernac/g_vernac.ml4 +++ b/vernac/g_vernac.ml4 @@ -20,7 +20,6 @@ open Extend open Decl_kinds open Declaremods open Declarations -open Misctypes open Namegen open Tok (* necessary for camlp5 *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 7f6270df1..94eb45fd3 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -29,7 +29,6 @@ open Decl_kinds open Constrexpr open Redexpr open Lemmas -open Misctypes open Locality open Vernacinterp @@ -637,7 +636,7 @@ let vernac_scheme l = let vernac_combined_scheme lid l = if Dumpglob.dump () then (Dumpglob.dump_definition lid false "def"; - List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ Misctypes.AN (make ?loc @@ Ident id))) l); + List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ AN (make ?loc @@ Ident id))) l); Indschemes.do_combined_scheme lid l let vernac_universe ~atts l = diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index f6199e820..3c88a3443 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -8,9 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Misctypes - -val dump_global : Libnames.reference or_by_notation -> unit +val dump_global : Libnames.reference Constrexpr.or_by_notation -> unit (** Vernacular entries *) val vernac_require : diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 9e8dfc4f8..5acac9e25 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Misctypes open Constrexpr open Libnames -- cgit v1.2.3 From 1dd682b1cafd64dd902e1ae6ea738192eb9b26db Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 2 Jun 2018 04:21:27 +0200 Subject: [api] Add compatiblity Misctypes module. To be removed in 8.10. --- .../07677-ejgallego-misctypes+bye2.sh | 8 +++ vernac/misctypes.ml | 75 ++++++++++++++++++++++ vernac/vernac.mllib | 2 + 3 files changed, 85 insertions(+) create mode 100644 dev/ci/user-overlays/07677-ejgallego-misctypes+bye2.sh create mode 100644 vernac/misctypes.ml diff --git a/dev/ci/user-overlays/07677-ejgallego-misctypes+bye2.sh b/dev/ci/user-overlays/07677-ejgallego-misctypes+bye2.sh new file mode 100644 index 000000000..b4f716139 --- /dev/null +++ b/dev/ci/user-overlays/07677-ejgallego-misctypes+bye2.sh @@ -0,0 +1,8 @@ +_OVERLAY_BRANCH=misctypes+bye2 + +if [ "$CI_PULL_REQUEST" = "7677" ] || [ "$CI_BRANCH" = "_OVERLAY_BRANCH" ]; then + + Equations_CI_BRANCH="$_OVERLAY_BRANCH" + Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + +fi diff --git a/vernac/misctypes.ml b/vernac/misctypes.ml new file mode 100644 index 000000000..ae725efaa --- /dev/null +++ b/vernac/misctypes.ml @@ -0,0 +1,75 @@ +(* Compat module, to be removed in 8.10 *) +open Names + +type lident = Names.lident +[@@ocaml.deprecated "use [Names.lident"] +type lname = Names.lname +[@@ocaml.deprecated "use [Names.lname]"] +type lstring = Names.lstring +[@@ocaml.deprecated "use [Names.lstring]"] + +type 'a or_by_notation_r = 'a Constrexpr.or_by_notation_r = + | AN of 'a [@ocaml.deprecated "use version in [Constrexpr]"] + | ByNotation of (string * string option) [@ocaml.deprecated "use version in [Constrexpr]"] +[@@ocaml.deprecated "use [Constrexpr.or_by_notation_r]"] + +type 'a or_by_notation = 'a Constrexpr.or_by_notation +[@@ocaml.deprecated "use [Constrexpr.or_by_notation]"] + +type intro_pattern_naming_expr = Namegen.intro_pattern_naming_expr = + | IntroIdentifier of Id.t [@ocaml.deprecated "Use version in [Evarutil]"] + | IntroFresh of Id.t [@ocaml.deprecated "Use version in [Evarutil]"] + | IntroAnonymous [@ocaml.deprecated "Use version in [Evarutil]"] +[@@ocaml.deprecated "use [Evarutil.intro_pattern_naming_expr]"] + +type 'a or_var = 'a Locus.or_var = + | ArgArg of 'a [@ocaml.deprecated "Use version in [Locus]"] + | ArgVar of Names.lident [@ocaml.deprecated "Use version in [Locus]"] +[@@ocaml.deprecated "use [Locus.or_var]"] + +type quantified_hypothesis = Tactypes.quantified_hypothesis = + AnonHyp of int [@ocaml.deprecated "Use version in [Tactypes]"] + | NamedHyp of Id.t [@ocaml.deprecated "Use version in [Tactypes]"] +[@@ocaml.deprecated "use [Tactypes.quantified_hypothesis]"] + +type multi = Equality.multi = + | Precisely of int [@ocaml.deprecated "use version in [Equality]"] + | UpTo of int [@ocaml.deprecated "use version in [Equality]"] + | RepeatStar [@ocaml.deprecated "use version in [Equality]"] + | RepeatPlus [@ocaml.deprecated "use version in [Equality]"] +[@@ocaml.deprecated "use [Equality.multi]"] + +type 'a bindings = 'a Tactypes.bindings = + | ImplicitBindings of 'a list [@ocaml.deprecated "use version in [Tactypes]"] + | ExplicitBindings of 'a Tactypes.explicit_bindings [@ocaml.deprecated "use version in [Tactypes]"] + | NoBindings [@ocaml.deprecated "use version in [Tactypes]"] +[@@ocaml.deprecated "use [Tactypes.bindings]"] + +type 'constr intro_pattern_expr = 'constr Tactypes.intro_pattern_expr = + | IntroForthcoming of bool [@ocaml.deprecated "use version in [Tactypes]"] + | IntroNaming of Namegen.intro_pattern_naming_expr [@ocaml.deprecated "use version in [Tactypes]"] + | IntroAction of 'constr Tactypes.intro_pattern_action_expr [@ocaml.deprecated "use version in [Tactypes]"] +and 'constr intro_pattern_action_expr = 'constr Tactypes.intro_pattern_action_expr = + | IntroWildcard [@ocaml.deprecated "use [Tactypes]"] + | IntroOrAndPattern of 'constr Tactypes.or_and_intro_pattern_expr [@ocaml.deprecated "use [Tactypes]"] + | IntroInjection of ('constr intro_pattern_expr) CAst.t list [@ocaml.deprecated "use [Tactypes]"] + | IntroApplyOn of 'constr CAst.t * 'constr intro_pattern_expr CAst.t [@ocaml.deprecated "use [Tactypes]"] + | IntroRewrite of bool [@ocaml.deprecated "use [Tactypes]"] +and 'constr or_and_intro_pattern_expr = 'constr Tactypes.or_and_intro_pattern_expr = + | IntroOrPattern of ('constr intro_pattern_expr) CAst.t list list [@ocaml.deprecated "use [Tactypes]"] + | IntroAndPattern of ('constr intro_pattern_expr) CAst.t list [@ocaml.deprecated "use [Tactypes]"] +[@@ocaml.deprecated "use version in [Tactypes]"] + +type 'id move_location = 'id Logic.move_location = + | MoveAfter of 'id [@ocaml.deprecated "use version in [Logic]"] + | MoveBefore of 'id [@ocaml.deprecated "use version in [Logic]"] + | MoveFirst [@ocaml.deprecated "use version in [Logic]"] + | MoveLast [@ocaml.deprecated "use version in [Logic]"] +[@@ocaml.deprecated "use version in [Logic]"] + +type 'a cast_type = 'a Glob_term.cast_type = + | CastConv of 'a [@ocaml.deprecated "use version in [Glob_term]"] + | CastVM of 'a [@ocaml.deprecated "use version in [Glob_term]"] + | CastCoerce [@ocaml.deprecated "use version in [Glob_term]"] + | CastNative of 'a [@ocaml.deprecated "use version in [Glob_term]"] +[@@ocaml.deprecated "use version in [Glob_term]"] diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 39c313ac7..356951b69 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -31,3 +31,5 @@ Vernacstate Mltop Topfmt Vernacentries + +Misctypes -- cgit v1.2.3