diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-07-20 17:10:58 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-07-25 16:07:32 +0200 |
| commit | fc218c26cfb226be25c344af50b4b86e52360934 (patch) | |
| tree | fd0650fa1fc981c81e62991d8d8e97431312285e | |
| parent | b6f3c8e4f173e3f272f966e1061e7112bf5d1b4a (diff) | |
[api] Remove type equalities from API.
This ensures that the API is self-contained and is, well, an API.
Before this patch, the contents of `API.mli` bore little relation with
what was used by the plugins [example: `Metasyntax` in tacentries.ml].
Many missing types had to be added.
A sanity check of the `API.mli` file can be done with:
`ocamlfind ocamlc -rectypes -package camlp5 -I lib API/API.mli`
37 files changed, 1331 insertions, 927 deletions
diff --git a/API/API.ml b/API/API.ml index fd20167f2..c952e123d 100644 --- a/API/API.ml +++ b/API/API.ml @@ -39,15 +39,15 @@ module Context = Context module Vars = Vars module Term = Term module Mod_subst = Mod_subst -(* module Cbytecodes *) +module Cbytecodes = Cbytecodes (* module Copcodes *) -(* module Cemitcodes *) +module Cemitcodes = Cemitcodes (* module Nativevalues *) (* module Primitives *) module Opaqueproof = Opaqueproof module Declareops = Declareops module Retroknowledge = Retroknowledge -(* module Conv_oracle *) +module Conv_oracle = Conv_oracle (* module Pre_env *) (* module Cbytegen *) (* module Nativelambda *) @@ -166,7 +166,7 @@ module Unification = Unification (* interp *) (******************************************************************************) module Stdarg = Stdarg -(* module Genintern *) +module Genintern = Genintern module Constrexpr_ops = Constrexpr_ops module Notation_ops = Notation_ops module Ppextend = Ppextend @@ -216,6 +216,15 @@ module Printer = Printer module Ppvernac = Ppvernac (******************************************************************************) +(* Parsing *) +(******************************************************************************) +module Tok = Tok +module CLexer = CLexer +module Pcoq = Pcoq +module Egramml = Egramml +(* Egramcoq *) + +(******************************************************************************) (* Tactics *) (******************************************************************************) (* module Dnet *) @@ -249,7 +258,7 @@ module Himsg = Himsg module ExplainErr = ExplainErr (* module Class *) module Locality = Locality -(* module Metasyntax *) +module Metasyntax = Metasyntax (* module Auto_ind_decl *) module Search = Search (* module Indschemes *) @@ -258,7 +267,7 @@ module Command = Command module Classes = Classes (* module Record *) (* module Assumptions *) -(* module Vernacinterp *) +module Vernacinterp = Vernacinterp module Mltop = Mltop module Topfmt = Topfmt module Vernacentries = Vernacentries @@ -268,3 +277,9 @@ module Vernacentries = Vernacentries (******************************************************************************) module Vernac_classifier = Vernac_classifier module Stm = Stm + +(******************************************************************************) +(* Highparsing *) +(******************************************************************************) +module G_vernac = G_vernac +module G_proofs = G_proofs diff --git a/API/API.mli b/API/API.mli index 309719539..f4eb520cf 100644 --- a/API/API.mli +++ b/API/API.mli @@ -33,21 +33,42 @@ end (************************************************************************) module Names : sig - module Id : module type of struct include Names.Id end - module MBId : sig - type t = Names.MBId.t + open Util + + module Id : + sig + type t val equal : t -> t -> bool - val to_id : t -> Names.Id.t - val repr : t -> int * Names.Id.t * Names.DirPath.t - val debug_to_string : t -> string - end + val compare : t -> t -> int + val hash : t -> int + val is_valid : string -> bool + val of_bytes : bytes -> t + val of_string : string -> t + val of_string_soft : string -> t + val to_string : t -> string + val print : t -> Pp.std_ppcmds - type evaluable_global_reference = Names.evaluable_global_reference = - | EvalVarRef of Id.t - | EvalConstRef of Names.Constant.t + module Set : Set.S with type elt = t + module Map : Map.ExtS with type key = t and module Set := Set + module Pred : Predicate.S with type elt = t + module List : List.MonoS with type elt = t + val hcons : t -> t + end - module Name : module type of struct include Names.Name end + module Name : + sig + type t = Anonymous (** anonymous identifier *) + | Name of Id.t (** non-anonymous identifier *) + val mk_name : Id.t -> t + val is_anonymous : t -> bool + val is_name : t -> bool + val compare : t -> t -> int + val equal : t -> t -> bool + val hash : t -> int + val hcons : t -> t + val print : t -> Pp.std_ppcmds + end type name = Name.t = | Anonymous @@ -56,7 +77,7 @@ sig module DirPath : sig - type t = Names.DirPath.t + type t val empty : t val make : Id.t list -> t val repr : t -> Id.t list @@ -64,23 +85,31 @@ sig val to_string : t -> string end + module MBId : sig + type t + val equal : t -> t -> bool + val to_id : t -> Id.t + val repr : t -> int * Id.t * DirPath.t + val debug_to_string : t -> string + end + module Label : sig - type t = Names.Label.t + type t val make : string -> t val equal : t -> t -> bool val compare : t -> t -> int - val of_id : Names.Id.t -> t - val to_id : t -> Names.Id.t + val of_id : Id.t -> t + val to_id : t -> Id.t val to_string : t -> string end module ModPath : sig - type t = Names.ModPath.t = - | MPfile of Names.DirPath.t - | MPbound of MBId.t - | MPdot of t * Label.t + type t = + | MPfile of DirPath.t + | MPbound of MBId.t + | MPdot of t * Label.t val compare : t -> t -> int val equal : t -> t -> bool val hash : t -> int @@ -91,7 +120,7 @@ sig module KerName : sig - type t = Names.KerName.t + type t val make : ModPath.t -> DirPath.t -> Label.t -> t val make2 : ModPath.t -> Label.t -> t val modpath : t -> ModPath.t @@ -108,40 +137,44 @@ sig module Constant : sig - type t = Names.Constant.t + type t val equal : t -> t -> bool - val make1 : Names.KerName.t -> t - val make2 : Names.ModPath.t -> Label.t -> t - val make3 : Names.ModPath.t -> Names.DirPath.t -> Label.t -> t - val repr3 : t -> Names.ModPath.t * Names.DirPath.t * Label.t - val canonical : t -> Names.KerName.t - val user : t -> Names.KerName.t + val make1 : KerName.t -> t + val make2 : ModPath.t -> Label.t -> t + val make3 : ModPath.t -> DirPath.t -> Label.t -> t + val repr3 : t -> ModPath.t * DirPath.t * Label.t + val canonical : t -> KerName.t + val user : t -> KerName.t val label : t -> Label.t end module MutInd : sig - type t = Names.MutInd.t - val make1 : Names.KerName.t -> t - val make2 : Names.ModPath.t -> Label.t -> t + type t + val make1 : KerName.t -> t + val make2 : ModPath.t -> Label.t -> t val equal : t -> t -> bool - val repr3 : t -> Names.ModPath.t * Names.DirPath.t * Label.t - val canonical : t -> Names.KerName.t - val modpath : t -> Names.ModPath.t + val repr3 : t -> ModPath.t * DirPath.t * Label.t + val canonical : t -> KerName.t + val modpath : t -> ModPath.t val label : t -> Label.t - val user : t -> Names.KerName.t + val user : t -> KerName.t val print : t -> Pp.std_ppcmds end module Projection : sig - type t = Names.Projection.t + type t val make : Constant.t -> bool -> t val map : (Constant.t -> Constant.t) -> t -> t val constant : t -> Constant.t val equal : t -> t -> bool end + type evaluable_global_reference = + | EvalVarRef of Id.t + | EvalConstRef of Constant.t + type inductive = MutInd.t * int val eq_ind : inductive -> inductive -> bool @@ -149,25 +182,31 @@ sig val eq_constructor : constructor -> constructor -> bool val constructor_hash : constructor -> int - module MPset : module type of struct include Names.MPset end - module MPmap : module type of struct include Names.MPmap end - module KNset : module type of struct include Names.KNset end - module KNmap : module type of struct include Names.KNmap end - module Cset : module type of struct include Names.Cset end - module Cset_env : module type of struct include Names.Cset_env end - module Cmap : module type of struct include Names.Cmap end - module Cmap_env : module type of struct include Names.Cmap_env end - module Cpred : module type of struct include Names.Cpred end - module Mindset : module type of struct include Names.Mindset end - module Mindmap : module type of struct include Names.Mindmap end - module Mindmap_env : module type of struct include Names.Mindmap_env end - module Indmap : module type of struct include Names.Indmap end - with type key = inductive - module Indmap_env : module type of struct include Names.Indmap_env end - module Constrmap : module type of struct include Names.Constrmap end - module Constrmap_env : module type of struct include Names.Constrmap_env end + module MPset : Set.S with type elt = ModPath.t + module MPmap : Map.ExtS with type key = ModPath.t and module Set := MPset + + module KNset : CSig.SetS with type elt = KerName.t + module KNpred : Predicate.S with type elt = KerName.t + module KNmap : Map.ExtS with type key = KerName.t and module Set := KNset + + module Cpred : Predicate.S with type elt = Constant.t + module Cset : CSig.SetS with type elt = Constant.t + module Cset_env : CSig.SetS with type elt = Constant.t + + module Cmap : Map.ExtS with type key = Constant.t and module Set := Cset + module Cmap_env : Map.ExtS with type key = Constant.t and module Set := Cset_env + + module Mindset : CSig.SetS with type elt = MutInd.t + module Mindmap : Map.ExtS with type key = MutInd.t and module Set := Mindset + module Mindmap_env : CSig.MapS with type key = MutInd.t + + module Indmap : CSig.MapS with type key = inductive + module Constrmap : CSig.MapS with type key = constructor + module Indmap_env : CSig.MapS with type key = inductive + module Constrmap_env : CSig.MapS with type key = constructor type transparent_state = Id.Pred.t * Cpred.t + val empty_transparent_state : transparent_state val full_transparent_state : transparent_state val var_full_transparent_state : transparent_state @@ -186,9 +225,8 @@ sig [@@ocaml.deprecated "alias of API.Names.ModPath.t"] type variable = Id.t - [@@ocaml.deprecated "alias of API.Names.Id.t"] - type 'a tableKey = 'a Names.tableKey = + type 'a tableKey = | ConstKey of 'a | VarKey of Id.t | RelKey of Int.t @@ -273,7 +311,9 @@ sig val debug_string_of_con : Constant.t -> string - module Idset : module type of struct include Id.Set end + type identifier = Id.t + module Idset : Set.S with type elt = identifier and type t = Id.Set.t + end module Univ : @@ -281,22 +321,30 @@ sig module Level : sig - type t = Univ.Level.t + type t val set : t val pr : t -> Pp.std_ppcmds end - module LSet : module type of struct include Univ.LSet end + type universe_level = Level.t + + module LSet : + sig + include CSig.SetS with type elt = universe_level + val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds + end module Universe : sig - type t = Univ.Universe.t + type t val pr : t -> Pp.std_ppcmds end + type universe = Universe.t + module Instance : sig - type t = Univ.Instance.t + type t val empty : t val of_array : Level.t array -> t val to_array : t -> Level.t array @@ -307,13 +355,19 @@ sig val out_punivs : 'a puniverses -> 'a - module Constraint : module type of struct include Univ.Constraint end + type constraint_type = Lt | Le | Eq + + type univ_constraint = universe_level * constraint_type * universe_level + + module Constraint : sig + include Set.S with type elt = univ_constraint + end type 'a constrained = 'a * Constraint.t module UContext : sig - type t = Univ.UContext.t + type t val empty : t end @@ -321,7 +375,7 @@ sig module AUContext : sig - type t = Univ.AUContext.t + type t val empty : t end @@ -329,20 +383,20 @@ sig module CumulativityInfo : sig - type t = Univ.CumulativityInfo.t + type t end type cumulativity_info = CumulativityInfo.t module ACumulativityInfo : sig - type t = Univ.ACumulativityInfo.t + type t end type abstract_cumulativity_info = ACumulativityInfo.t module ContextSet : sig - type t = Univ.ContextSet.t + type t val empty : t val of_context : UContext.t -> t val to_context : t -> UContext.t @@ -350,15 +404,26 @@ sig type 'a in_universe_context_set = 'a * ContextSet.t type 'a in_universe_context = 'a * UContext.t - type constraint_type = Univ.constraint_type type universe_context_set = ContextSet.t type universe_set = LSet.t type 'a constraint_function = 'a -> 'a -> Constraint.t -> Constraint.t - type universe_subst = Univ.universe_subst - type universe_level_subst = Univ.universe_level_subst + + module LMap : + sig + include CMap.ExtS with type key = universe_level and module Set := LSet + + val union : 'a t -> 'a t -> 'a t + val diff : 'a t -> 'a t -> 'a t + val subst_union : 'a option t -> 'a option t -> 'a option t + val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds + end + + type 'a universe_map = 'a LMap.t + type universe_subst = universe universe_map + type universe_level_subst = universe_level universe_map val enforce_leq : Universe.t constraint_function val pr_uni : Universe.t -> Pp.std_ppcmds @@ -371,33 +436,33 @@ end module UGraph : sig - type t = UGraph.t + type t val pr_universes : (Univ.Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds end module Esubst : sig - type 'a subs = 'a Esubst.subs + type 'a subs val subs_id : int -> 'a subs end module Sorts : sig - type contents = Sorts.contents = Pos | Null - type t = Sorts.t = + type contents = Pos | Null + type t = | Prop of contents | Type of Univ.Universe.t val is_prop : t -> bool val hash : t -> int - type family = Sorts.family = InProp | InSet | InType + type family = InProp | InSet | InType val family : t -> family end module Evar : sig (** Unique identifier of some {i evar} *) - type t = Evar.t + type t (** Recover the underlying integer. *) val repr : t -> int @@ -405,7 +470,8 @@ sig val equal : t -> t -> bool (** a set of unique identifiers of some {i evars} *) - module Set : module type of struct include Evar.Set end + module Set : Set.S with type elt = t + module Map : CMap.ExtS with type key = t and module Set := Set end @@ -413,12 +479,12 @@ module Constr : sig open Names - type t = Constr.t + type t type constr = t type types = t - type cast_kind = Constr.cast_kind = + type cast_kind = | VMcast | NATIVEcast | DEFAULTcast @@ -443,16 +509,16 @@ sig type ('constr, 'types) pcofixpoint = int * ('constr, 'types) prec_declaration - type case_style = Constr.case_style = + type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle (** infer printing form from number of constructor *) - type case_printing = Constr.case_printing = + type case_printing = { ind_tags : bool list; (** tell whether letin or lambda in the arity of the inductive type *) cstr_tags : bool list array; (** tell whether letin or lambda in the signature of each constructor *) style : case_style } - type case_info = Constr.case_info = + type case_info = { ci_ind : inductive; (* inductive type to which belongs the value that is being matched *) ci_npar : int; (* number of parameters of the above inductive type *) ci_cstr_ndecls : int array; (* For each constructor, the corresponding integer determines @@ -466,7 +532,7 @@ sig ci_pp_info : case_printing (* not interpreted by the kernel *) } - type ('constr, 'types, 'sort, 'univs) kind_of_term = ('constr, 'types, 'sort, 'univs) Constr.kind_of_term = + type ('constr, 'types, 'sort, 'univs) kind_of_term = | Rel of int | Var of Id.t | Meta of metavariable @@ -531,7 +597,7 @@ sig sig (* local declaration *) (* local declaration *) - type ('constr, 'types) pt = ('constr, 'types) Context.Rel.Declaration.pt = + type ('constr, 'types) pt = | LocalAssum of Names.Name.t * 'types (** name, type *) | LocalDef of Names.Name.t * 'constr * 'types (** name, value, type *) @@ -625,7 +691,7 @@ sig module Declaration : sig (** local declaration *) - type ('constr, 'types) pt = ('constr, 'types) Context.Named.Declaration.pt = + type ('constr, 'types) pt = | LocalAssum of Names.Id.t * 'types (** identifier, type *) | LocalDef of Names.Id.t * 'constr * 'types (** identifier, value, type *) @@ -752,7 +818,6 @@ module Term : sig type sorts_family = Sorts.family = InProp | InSet | InType - [@@deprecated "alias of API.Sorts.family"] type contents = Sorts.contents = Pos | Null @@ -779,19 +844,18 @@ sig type pconstant = Names.Constant.t puniverses type pinductive = Names.inductive puniverses type pconstructor = Names.constructor puniverses - type case_style = Term.case_style = - | LetStyle - | IfStyle - | LetPatternStyle - | MatchStyle - | RegularStyle - + type case_style = Constr.case_style = + | LetStyle + | IfStyle + | LetPatternStyle + | MatchStyle + | RegularStyle - type case_printing = Term.case_printing = - { ind_tags : bool list; - cstr_tags : bool list array; - style : case_style - } + type case_printing = Constr.case_printing = + { ind_tags : bool list; + cstr_tags : bool list array; + style : case_style + } type case_info = Constr.case_info = { ci_ind : Names.inductive; @@ -803,8 +867,10 @@ sig type ('constr, 'types) pfixpoint = (int array * int) * ('constr, 'types) prec_declaration + type ('constr, 'types) pcofixpoint = int * ('constr, 'types) prec_declaration + type ('constr, 'types, 'sort, 'univs) kind_of_term = ('constr, 'types, 'sort, 'univs) Constr.kind_of_term = | Rel of int | Var of Names.Id.t @@ -917,12 +983,12 @@ sig *) val eq_constr_nounivs : constr -> constr -> bool - type ('constr, 'types) kind_of_type = ('constr, 'types) Term.kind_of_type = - | SortType of Sorts.t - | CastType of 'types * 'types - | ProdType of Names.Name.t * 'types * 'types - | LetInType of Names.Name.t * 'constr * 'types * 'types - | AtomicType of 'constr * 'constr array + type ('constr, 'types) kind_of_type = + | SortType of Sorts.t + | CastType of 'types * 'types + | ProdType of Names.Name.t * 'types * 'types + | LetInType of Names.Name.t * 'constr * 'types * 'types + | AtomicType of 'constr * 'constr array val kind_of_type : types -> (constr, types) kind_of_type @@ -952,9 +1018,9 @@ end module Mod_subst : sig - type substitution = Mod_subst.substitution - type 'a substituted = 'a Mod_subst.substituted - type delta_resolver = Mod_subst.delta_resolver + type delta_resolver + type substitution + type 'a substituted val force_constr : Constr.t substituted -> Constr.t @@ -973,25 +1039,38 @@ end module Opaqueproof : sig - type opaquetab = Opaqueproof.opaquetab - type opaque = Opaqueproof.opaque + type opaquetab + type opaque val empty_opaquetab : opaquetab val force_proof : opaquetab -> opaque -> Constr.t end +module Cbytecodes : +sig + type tag = int + type reloc_table = (tag * int) array +end + +module Cemitcodes : +sig + type to_patch_substituted +end + module Decl_kinds : sig type polymorphic = bool type cumulative_inductive_flag = bool - type recursivity_kind = Decl_kinds.recursivity_kind = + type recursivity_kind = | Finite | CoFinite | BiFinite - type locality = Decl_kinds.locality = + + type locality = | Discharge | Local | Global - type definition_object_kind = Decl_kinds.definition_object_kind = + + type definition_object_kind = | Definition | Coercion | SubClass @@ -1004,7 +1083,7 @@ sig | IdentityCoercion | Instance | Method - type theorem_kind = Decl_kinds.theorem_kind = + type theorem_kind = | Theorem | Lemma | Fact @@ -1012,19 +1091,19 @@ sig | Property | Proposition | Corollary - type goal_object_kind = Decl_kinds.goal_object_kind = + type goal_object_kind = | DefinitionBody of definition_object_kind | Proof of theorem_kind type goal_kind = locality * polymorphic * goal_object_kind - type assumption_object_kind = Decl_kinds.assumption_object_kind = + type assumption_object_kind = | Definitional | Logical | Conjectural - type logical_kind = Decl_kinds.logical_kind = + type logical_kind = | IsAssumption of assumption_object_kind | IsDefinition of definition_object_kind | IsProof of theorem_kind - type binding_kind = Decl_kinds.binding_kind = + type binding_kind = | Explicit | Implicit type private_flag = bool @@ -1033,12 +1112,12 @@ end module Retroknowledge : sig - type action = Retroknowledge.action - type nat_field = Retroknowledge.nat_field = + type action + type nat_field = | NatType | NatPlus | NatTimes - type n_field = Retroknowledge.n_field = + type n_field = | NPositive | NType | NTwice @@ -1047,7 +1126,7 @@ sig | NPhiInv | NPlus | NTimes - type int31_field = Retroknowledge.int31_field = + type int31_field = | Int31Bits | Int31Type | Int31Constructor @@ -1073,44 +1152,60 @@ sig | Int31Lor | Int31Land | Int31Lxor - type field = Retroknowledge.field = + type field = | KInt31 of string * int31_field end +module Conv_oracle : +sig + type level +end + module Declarations : sig - type recarg = Declarations.recarg = + + open Names + + type recarg = | Norec | Mrec of Names.inductive | Imbr of Names.inductive type wf_paths = recarg Rtree.t - type inline = Declarations.inline - type constant_def = Declarations.constant_def = + type inline = int option + type constant_def = | Undef of inline | Def of Constr.t Mod_subst.substituted | OpaqueDef of Opaqueproof.opaque - type template_arity = Declarations.template_arity = { + type template_arity = { template_param_levels : Univ.Level.t option list; template_level : Univ.Universe.t; } - type ('a, 'b) declaration_arity = ('a, 'b) Declarations.declaration_arity = + type ('a, 'b) declaration_arity = | RegularArity of 'a | TemplateArity of 'b type constant_type = (Constr.types, Context.Rel.t * template_arity) declaration_arity - type constant_universes = Declarations.constant_universes - type projection_body = Declarations.projection_body = { + + type constant_universes = + | Monomorphic_const of Univ.universe_context + | Polymorphic_const of Univ.abstract_universe_context + + type projection_body = { proj_ind : Names.MutInd.t; proj_npars : int; proj_arg : int; proj_type : Constr.types; - proj_eta : Constr.t * Constr.types; + proj_eta : Constr.t * Constr.types; proj_body : Constr.t; } - type typing_flags = Declarations.typing_flags - type constant_body = Declarations.constant_body = { + type typing_flags = { + check_guarded : bool; + check_universes : bool; + } + + type constant_body = { const_hyps : Context.Named.t; const_body : constant_def; const_type : constant_type; @@ -1120,10 +1215,18 @@ sig const_inline_code : bool; const_typing_flags : typing_flags; } - type one_inductive_body = Declarations.one_inductive_body = { + + type regular_inductive_arity = { + mind_user_arity : Constr.types; + mind_sort : Sorts.t; + } + + type inductive_arity = (regular_inductive_arity, template_arity) declaration_arity + + type one_inductive_body = { mind_typename : Names.Id.t; mind_arity_ctxt : Context.Rel.t; - mind_arity : Declarations.inductive_arity; + mind_arity : inductive_arity; mind_consnames : Names.Id.t array; mind_user_lc : Constr.types array; mind_nrealargs : int; @@ -1137,43 +1240,47 @@ sig mind_nb_args : int; mind_reloc_tbl : Cbytecodes.reloc_table; } - type ('ty,'a) functorize = ('ty,'a) Declarations.functorize = + + type ('ty,'a) functorize = | NoFunctor of 'a | MoreFunctor of Names.MBId.t * 'ty * ('ty,'a) functorize - type with_declaration = Declarations.with_declaration = + + type with_declaration = | WithMod of Names.Id.t list * Names.ModPath.t | WithDef of Names.Id.t list * Constr.t Univ.in_universe_context - type module_alg_expr = Declarations.module_alg_expr = + type module_alg_expr = | MEident of Names.ModPath.t | MEapply of module_alg_expr * Names.ModPath.t | MEwith of module_alg_expr * with_declaration - type abstract_inductive_universes = Declarations.abstract_inductive_universes = + type abstract_inductive_universes = | Monomorphic_ind of Univ.universe_context | Polymorphic_ind of Univ.abstract_universe_context | Cumulative_ind of Univ.abstract_cumulativity_info - type mutual_inductive_body = Declarations.mutual_inductive_body = { + type record_body = (Id.t * Constant.t array * projection_body array) option + + type mutual_inductive_body = { mind_packets : one_inductive_body array; - mind_record : Declarations.record_body option; + mind_record : record_body option; mind_finite : Decl_kinds.recursivity_kind; mind_ntypes : int; mind_hyps : Context.Named.t; mind_nparams : int; mind_nparams_rec : int; mind_params_ctxt : Context.Rel.t; - mind_universes : Declarations.abstract_inductive_universes; + mind_universes : abstract_inductive_universes; mind_private : bool option; - mind_typing_flags : Declarations.typing_flags; + mind_typing_flags : typing_flags; } and module_expression = (module_type_body,module_alg_expr) functorize - and module_implementation = Declarations.module_implementation = + and module_implementation = | Abstract | Algebraic of module_expression | Struct of module_signature | FullStruct - and module_body = Declarations.module_body = + and module_body = { mod_mp : Names.ModPath.t; mod_expr : module_implementation; mod_type : module_signature; @@ -1185,7 +1292,7 @@ sig and module_signature = (module_type_body,structure_body) functorize and module_type_body = module_body and structure_body = (Names.Label.t * structure_field_body) list - and structure_field_body = Declarations.structure_field_body = + and structure_field_body = | SFBconst of constant_body | SFBmind of mutual_inductive_body | SFBmodule of module_body @@ -1201,11 +1308,44 @@ end module Entries : sig - type mutual_inductive_entry = Entries.mutual_inductive_entry + + open Names + open Constr + + type local_entry = + | LocalDefEntry of constr + | LocalAssumEntry of constr + + type inductive_universes = + | Monomorphic_ind_entry of Univ.universe_context + | Polymorphic_ind_entry of Univ.universe_context + | Cumulative_ind_entry of Univ.cumulativity_info + + type one_inductive_entry = { + mind_entry_typename : Id.t; + mind_entry_arity : constr; + mind_entry_template : bool; (* Use template polymorphism *) + mind_entry_consnames : Id.t list; + mind_entry_lc : constr list } + + type mutual_inductive_entry = { + mind_entry_record : (Names.Id.t option) option; + (** Some (Some id): primitive record with id the binder name of the record + in projections. + Some None: non-primitive record *) + mind_entry_finite : Decl_kinds.recursivity_kind; + mind_entry_params : (Id.t * local_entry) list; + mind_entry_inds : one_inductive_entry list; + mind_entry_universes : inductive_universes; + (* universe constraints and the constraints for subtyping of + inductive types in the block. *) + mind_entry_private : bool option; + } + type inline = int option type 'a proof_output = Constr.t Univ.in_universe_context_set * 'a type 'a const_entry_body = 'a proof_output Future.computation - type 'a definition_entry = 'a Entries.definition_entry = + type 'a definition_entry = { const_entry_body : 'a const_entry_body; (* List of section variables *) const_entry_secctx : Context.Named.t option; @@ -1217,8 +1357,12 @@ sig const_entry_opaque : bool; const_entry_inline_code : bool } type parameter_entry = Context.Named.t option * bool * Constr.types Univ.in_universe_context * inline - type projection_entry = Entries.projection_entry - type 'a constant_entry = 'a Entries.constant_entry = + + type projection_entry = { + proj_entry_ind : MutInd.t; + proj_entry_arg : int } + + type 'a constant_entry = | DefinitionEntry of 'a definition_entry | ParameterEntry of parameter_entry | ProjectionEntry of projection_entry @@ -1226,14 +1370,15 @@ end module Environ : sig - type env = Environ.env - type named_context_val = Environ.named_context_val - type ('constr, 'types) punsafe_judgment = ('constr, 'types) Environ.punsafe_judgment = + type env + type named_context_val + + type ('constr, 'types) punsafe_judgment = { uj_val : 'constr; uj_type : 'types } - type 'types punsafe_type_judgment = 'types Environ.punsafe_type_judgment = { + type 'types punsafe_type_judgment = { utj_val : 'types; utj_type : Sorts.t } @@ -1245,7 +1390,7 @@ sig val push_rec_types : Term.rec_declaration -> env -> env val lookup_rel : int -> env -> Context.Rel.Declaration.t val lookup_named : Names.Id.t -> env -> Context.Named.Declaration.t - val lookup_named_val : Names.Id.t -> Environ.named_context_val -> Context.Named.Declaration.t + val lookup_named_val : Names.Id.t -> named_context_val -> Context.Named.Declaration.t val lookup_constant : Names.Constant.t -> env -> Declarations.constant_body val opaque_tables : env -> Opaqueproof.opaquetab val is_projection : Names.Constant.t -> env -> bool @@ -1262,16 +1407,18 @@ sig val constant_opt_value_in : env -> Names.Constant.t Univ.puniverses -> Constr.t option val fold_named_context_reverse : ('a -> Context.Named.Declaration.t -> 'a) -> init:'a -> env -> 'a - val evaluable_named : Names.Id.t -> Environ.env -> bool + val evaluable_named : Names.Id.t -> env -> bool val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env end module CClosure : sig - type fconstr = CClosure.fconstr - type clos_infos = CClosure.clos_infos + type table_key = Names.Constant.t Univ.puniverses Names.tableKey - type fterm = CClosure.fterm = + + type fconstr + + type fterm = | FRel of int | FAtom of Constr.t (** Metas and Sorts *) | FCast of fconstr * Constr.cast_kind * fconstr @@ -1290,18 +1437,27 @@ sig | FLIFT of int * fconstr | FCLOS of Constr.t * fconstr Esubst.subs | FLOCKED + module RedFlags : sig - type reds = CClosure.RedFlags.reds - type red_kind = CClosure.RedFlags.red_kind + type reds + type red_kind val mkflags : red_kind list -> reds val fBETA : red_kind val fCOFIX : red_kind - val fCONST : Names.Constant.t -> CClosure.RedFlags.red_kind + val fCONST : Names.Constant.t -> red_kind val fFIX : red_kind val fMATCH : red_kind val fZETA : red_kind val red_add_transparent : reds -> Names.transparent_state -> reds end + + type 'a infos_cache + type 'a infos = { + i_flags : RedFlags.reds; + i_cache : 'a infos_cache } + + type clos_infos = fconstr infos + val mk_clos : fconstr Esubst.subs -> Constr.t -> fconstr val mk_atom : Constr.t -> fconstr val mk_clos_deep : @@ -1326,7 +1482,7 @@ end module Reduction : sig exception NotConvertible - type conv_pb = Reduction.conv_pb = + type conv_pb = | CONV | CUMUL @@ -1347,7 +1503,59 @@ end module Type_errors : sig - type type_error = Type_errors.type_error + + open Names + open Term + open Environ + + type 'constr pguard_error = + (** Fixpoints *) + | NotEnoughAbstractionInFixBody + | RecursionNotOnInductiveType of 'constr + | RecursionOnIllegalTerm of int * (env * 'constr) * int list * int list + | NotEnoughArgumentsForFixCall of int + (** CoFixpoints *) + | CodomainNotInductiveType of 'constr + | NestedRecursiveOccurrences + | UnguardedRecursiveCall of 'constr + | RecCallInTypeOfAbstraction of 'constr + | RecCallInNonRecArgOfConstructor of 'constr + | RecCallInTypeOfDef of 'constr + | RecCallInCaseFun of 'constr + | RecCallInCaseArg of 'constr + | RecCallInCasePred of 'constr + | NotGuardedForm of 'constr + | ReturnPredicateNotCoInductive of 'constr + + type arity_error = + | NonInformativeToInformative + | StrongEliminationOnNonSmallType + | WrongArity + + type ('constr, 'types) ptype_error = + | UnboundRel of int + | UnboundVar of variable + | NotAType of ('constr, 'types) punsafe_judgment + | BadAssumption of ('constr, 'types) punsafe_judgment + | ReferenceVariables of identifier * 'constr + | ElimArity of pinductive * sorts_family list * 'constr * ('constr, 'types) punsafe_judgment + * (sorts_family * sorts_family * arity_error) option + | CaseNotInductive of ('constr, 'types) punsafe_judgment + | WrongCaseInfo of pinductive * case_info + | NumberBranches of ('constr, 'types) punsafe_judgment * int + | IllFormedBranch of 'constr * pconstructor * 'constr * 'constr + | Generalization of (Name.t * 'types) * ('constr, 'types) punsafe_judgment + | ActualType of ('constr, 'types) punsafe_judgment * 'types + | CantApplyBadType of + (int * 'constr * 'constr) * ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array + | CantApplyNonFunctional of ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array + | IllFormedRecBody of 'constr pguard_error * Name.t array * int * env * ('constr, 'types) punsafe_judgment array + | IllTypedRecBody of + int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array + | UnsatisfiedConstraints of Univ.Constraint.t + + type type_error = (constr, types) ptype_error + exception TypeError of Environ.env * type_error end @@ -1387,8 +1595,8 @@ end module Safe_typing : sig - type private_constants = Safe_typing.private_constants - val mk_pure_proof : Constr.t -> Safe_typing.private_constants Entries.proof_output + type private_constants + val mk_pure_proof : Constr.t -> private_constants Entries.proof_output end (************************************************************************) @@ -1406,88 +1614,99 @@ sig type advanced_flag = bool type rec_flag = bool - type 'a or_by_notation = 'a Misctypes.or_by_notation = + type 'a or_by_notation = | AN of 'a | ByNotation of (string * string option) Loc.located - type 'a or_var = 'a Misctypes.or_var = + + type 'a or_var = | ArgArg of 'a | ArgVar of Names.Id.t Loc.located + type 'a and_short_name = 'a * Names.Id.t Loc.located option - type glob_level = Misctypes.glob_level - type 'a glob_sort_gen = 'a Misctypes.glob_sort_gen = - | GProp - | GSet - | GType of 'a + + type 'a glob_sort_gen = + | GProp (** representation of [Prop] literal *) + | GSet (** representation of [Set] literal *) + | GType of 'a (** representation of [Type] literal *) + + type level_info = Names.Name.t Loc.located option + type glob_level = level_info glob_sort_gen + type sort_info = Names.Name.t Loc.located list type glob_sort = sort_info glob_sort_gen - type 'a cast_type = 'a Misctypes.cast_type = + + type case_style = Term.case_style = + | LetStyle + | IfStyle + | LetPatternStyle + | MatchStyle + | RegularStyle (** infer printing form from number of constructor *) + + type 'a cast_type = | CastConv of 'a | CastVM of 'a | CastCoerce | CastNative of 'a - type 'constr intro_pattern_expr = 'constr Misctypes.intro_pattern_expr = + + type 'constr intro_pattern_expr = | IntroForthcoming of bool | IntroNaming of intro_pattern_naming_expr | IntroAction of 'constr intro_pattern_action_expr - and intro_pattern_naming_expr = Misctypes.intro_pattern_naming_expr = - | IntroIdentifier of Names.Id.t - | IntroFresh of Names.Id.t - | IntroAnonymous - and 'constr intro_pattern_action_expr = 'constr Misctypes.intro_pattern_action_expr = - | IntroWildcard - | IntroOrAndPattern of 'constr or_and_intro_pattern_expr - | IntroInjection of ('constr intro_pattern_expr) Loc.located list - | IntroApplyOn of 'constr Loc.located * 'constr intro_pattern_expr Loc.located - | IntroRewrite of bool - and 'constr or_and_intro_pattern_expr = 'constr Misctypes.or_and_intro_pattern_expr = - | IntroOrPattern of ('constr intro_pattern_expr) Loc.located list list - | IntroAndPattern of ('constr intro_pattern_expr) Loc.located list - type quantified_hypothesis = Misctypes.quantified_hypothesis = + and intro_pattern_naming_expr = + | IntroIdentifier of Names.Id.t + | IntroFresh of Names.Id.t + | IntroAnonymous + and 'constr intro_pattern_action_expr = + | IntroWildcard + | IntroOrAndPattern of 'constr or_and_intro_pattern_expr + | IntroInjection of ('constr intro_pattern_expr) Loc.located list + | IntroApplyOn of 'constr Loc.located * 'constr intro_pattern_expr Loc.located + | IntroRewrite of bool + and 'constr or_and_intro_pattern_expr = + | IntroOrPattern of ('constr intro_pattern_expr) Loc.located list list + | IntroAndPattern of ('constr intro_pattern_expr) Loc.located list + + type quantified_hypothesis = | AnonHyp of int | NamedHyp of Names.Id.t + type 'a explicit_bindings = (quantified_hypothesis * 'a) Loc.located list - type 'a bindings = 'a Misctypes.bindings = + + type 'a bindings = | ImplicitBindings of 'a list | ExplicitBindings of 'a explicit_bindings | NoBindings + type 'a with_bindings = 'a * 'a bindings - type 'a core_destruction_arg = 'a Misctypes.core_destruction_arg = + + type 'a core_destruction_arg = | ElimOnConstr of 'a | ElimOnIdent of Names.Id.t Loc.located | ElimOnAnonHyp of int - type inversion_kind = Misctypes.inversion_kind = + + type inversion_kind = | SimpleInversion | FullInversion | FullInversionClear - type multi = Misctypes.multi = + + type multi = | Precisely of int | UpTo of int | RepeatStar | RepeatPlus - type 'id move_location = 'id Misctypes.move_location = + type 'id move_location = | MoveAfter of 'id | MoveBefore of 'id | MoveFirst | MoveLast + type 'a destruction_arg = clear_flag * 'a core_destruction_arg -end -module Extend : -sig - type ('self, 'a) symbol = ('self, 'a) Extend.symbol - type 'a user_symbol = 'a Extend.user_symbol = - | Ulist1 of 'a user_symbol - | Ulist1sep of 'a user_symbol * string - | Ulist0 of 'a user_symbol - | Ulist0sep of 'a user_symbol * string - | Uopt of 'a user_symbol - | Uentry of 'a - | Uentryl of 'a * int end module Locus : sig - type 'a occurrences_gen = 'a Locus.occurrences_gen = + type 'a occurrences_gen = | AllOccurrences | AllOccurrencesBut of 'a list (** non-empty *) | NoOccurrences @@ -1495,10 +1714,10 @@ sig type occurrences = int occurrences_gen type occurrences_expr = (int Misctypes.or_var) occurrences_gen type 'a with_occurrences = occurrences_expr * 'a - type hyp_location_flag = Locus.hyp_location_flag = + type hyp_location_flag = InHyp | InHypTypeOnly | InHypValueOnly type 'a hyp_location_expr = 'a with_occurrences * hyp_location_flag - type 'id clause_expr = 'id Locus.clause_expr = + type 'id clause_expr = { onhyps : 'id hyp_location_expr list option; concl_occs : occurrences_expr } type clause = Names.Id.t clause_expr @@ -1547,14 +1766,18 @@ end module Libnames : sig - type full_path = Libnames.full_path - val pr_path : Libnames.full_path -> Pp.std_ppcmds + + open Util + open Names + + type full_path + val pr_path : full_path -> Pp.std_ppcmds val make_path : Names.DirPath.t -> Names.Id.t -> full_path val eq_full_path : full_path -> full_path -> bool val dirpath : full_path -> Names.DirPath.t val path_of_string : string -> full_path - type qualid = Libnames.qualid + type qualid val make_qualid : Names.DirPath.t -> Names.Id.t -> qualid val qualid_eq : qualid -> qualid -> bool val repr_qualid : qualid -> Names.DirPath.t * Names.Id.t @@ -1565,8 +1788,8 @@ sig val qualid_of_dirpath : Names.DirPath.t -> qualid val qualid_of_ident : Names.Id.t -> qualid - type reference = Libnames.reference = - | Qualid of Libnames.qualid Loc.located + type reference = + | Qualid of qualid Loc.located | Ident of Names.Id.t Loc.located val loc_of_reference : reference -> Loc.t option val qualid_of_reference : reference -> qualid Loc.located @@ -1580,23 +1803,26 @@ sig val string_of_path : full_path -> string val basename : full_path -> Names.Id.t - type object_name = Libnames.full_path * Names.KerName.t + type object_name = full_path * Names.KerName.t type object_prefix = Names.DirPath.t * (Names.ModPath.t * Names.DirPath.t) - module Dirset : module type of struct include Libnames.Dirset end - module Dirmap : module type of struct include Libnames.Dirmap end - module Spmap : module type of struct include Libnames.Spmap end + module Dirset : Set.S with type elt = DirPath.t + module Dirmap : Map.ExtS with type key = DirPath.t and module Set := Dirset + module Spmap : CSig.MapS with type key = full_path end module Globnames : sig - type global_reference = Globnames.global_reference = + + open Util + + type global_reference = | VarRef of Names.Id.t | ConstRef of Names.Constant.t | IndRef of Names.inductive | ConstructRef of Names.constructor - type extended_global_reference = Globnames.extended_global_reference = + type extended_global_reference = | TrueGlobal of global_reference | SynDef of Names.KerName.t @@ -1606,10 +1832,14 @@ sig * - pretty printing (of user provided names/aliases) are implemented by * the _env ones *) - module Refset : module type of struct include Globnames.Refset end - module Refmap : module type of struct include Globnames.Refmap end - module Refset_env : module type of struct include Globnames.Refset_env end - module Refmap_env : module type of struct include Globnames.Refmap_env end + module Refset : CSig.SetS with type elt = global_reference + module Refmap : Map.ExtS + with type key = global_reference and module Set := Refset + + module Refset_env : CSig.SetS with type elt = global_reference + module Refmap_env : Map.ExtS + with type key = global_reference and module Set := Refset_env + module RefOrdered : sig type t = global_reference @@ -1626,7 +1856,7 @@ sig val global_of_constr : Constr.t -> global_reference val subst_global : Mod_subst.substitution -> global_reference -> global_reference * Constr.t - val destConstructRef : Globnames.global_reference -> Names.constructor + val destConstructRef : global_reference -> Names.constructor val reference_of_constr : Constr.t -> global_reference [@@ocaml.deprecated "alias of API.Globnames.global_of_constr"] @@ -1636,14 +1866,14 @@ end module Libobject : sig - type obj = Libobject.obj - type 'a substitutivity = 'a Libobject.substitutivity = + type obj + type 'a substitutivity = | Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a - type 'a object_declaration = 'a Libobject.object_declaration = - { + + type 'a object_declaration = { object_name : string; cache_function : Libnames.object_name * 'a -> unit; load_function : int -> Libnames.object_name * 'a -> unit; @@ -1661,18 +1891,19 @@ end module Summary : sig - type frozen = Summary.frozen + type frozen + type marshallable - type marshallable = Summary.marshallable - type 'a summary_declaration = 'a Summary.summary_declaration = + type 'a summary_declaration = { freeze_function : marshallable -> 'a; unfreeze_function : 'a -> unit; init_function : unit -> unit; } + val ref : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref val declare_summary : string -> 'a summary_declaration -> unit module Local : sig - type 'a local_ref = 'a Summary.Local.local_ref + type 'a local_ref val ref : ?freeze:('a -> 'a) -> name:string -> 'a -> 'a local_ref val (:=) : 'a local_ref -> 'a -> unit val (!) : 'a local_ref -> 'a @@ -1696,9 +1927,9 @@ sig val shortest_qualid_of_tactic : Names.KerName.t -> Libnames.qualid val basename_of_global : Globnames.global_reference -> Names.Id.t - type visibility = Nametab.visibility = - | Until of int - | Exactly of int + type visibility = + | Until of int + | Exactly of int val push_tactic : visibility -> Libnames.full_path -> Names.KerName.t -> unit val error_global_not_found : ?loc:Loc.t -> Libnames.qualid -> 'a @@ -1739,7 +1970,7 @@ end module Lib : sig type is_type = bool type export = bool option - type node = Lib.node = + type node = | Leaf of Libobject.obj (* FIX: horrible hack (wrt. Enrico) *) | CompilingLibrary of Libnames.object_prefix | OpenedModule of is_type * export * Libnames.object_prefix * Summary.frozen @@ -1790,7 +2021,7 @@ end module Goptions : sig type option_name = string list - type 'a option_sig = 'a Goptions.option_sig = + type 'a option_sig = { optdepr : bool; optname : string; @@ -1798,7 +2029,9 @@ sig optread : unit -> 'a; optwrite : 'a -> unit } - type 'a write_function = 'a Goptions.write_function + + type 'a write_function = 'a -> unit + val declare_bool_option : ?preprocess:(bool -> bool) -> bool option_sig -> bool write_function val declare_int_option : ?preprocess:(int option -> int option) -> @@ -1810,7 +2043,7 @@ end module Keys : sig - type key = Keys.key + type key val constr_key : ('a -> ('a, 't, 'u, 'i) Constr.kind_of_term) -> 'a -> key option val declare_equiv_keys : key -> key -> unit val pr_keys : (Globnames.global_reference -> Pp.std_ppcmds) -> Pp.std_ppcmds @@ -1818,14 +2051,16 @@ end module Coqlib : sig - type coq_eq_data = Coqlib.coq_eq_data = { eq : Globnames.global_reference; - ind : Globnames.global_reference; - refl : Globnames.global_reference; - sym : Globnames.global_reference; - trans: Globnames.global_reference; - congr: Globnames.global_reference; - } - type coq_sigma_data = Coqlib.coq_sigma_data = { + + type coq_eq_data = { eq : Globnames.global_reference; + ind : Globnames.global_reference; + refl : Globnames.global_reference; + sym : Globnames.global_reference; + trans: Globnames.global_reference; + congr: Globnames.global_reference; + } + + type coq_sigma_data = { proj1 : Globnames.global_reference; proj2 : Globnames.global_reference; elim : Globnames.global_reference; @@ -1878,8 +2113,8 @@ end module Universes : sig - type universe_binders = Universes.universe_binders - type universe_opt_subst = Universes.universe_opt_subst + type universe_binders + type universe_opt_subst val fresh_inductive_instance : Environ.env -> Names.inductive -> Term.pinductive Univ.in_universe_context_set val new_Type : Names.DirPath.t -> Term.types val type_of_global : Globnames.global_reference -> Term.types Univ.in_universe_context_set @@ -1888,11 +2123,11 @@ sig val new_sort_in_family : Sorts.family -> Sorts.t val pr_with_global_universes : Univ.Level.t -> Pp.std_ppcmds val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds - type universe_constraint = Universes.universe_constraint + type universe_constraint module Constraints : sig - type t = Universes.Constraints.t + type t val pr : t -> Pp.std_ppcmds end @@ -1901,28 +2136,29 @@ end module UState : sig - type t = UState.t + type t val context : t -> Univ.UContext.t val context_set : t -> Univ.ContextSet.t val of_context_set : Univ.ContextSet.t -> t - type rigid = UState.rigid = + type rigid = | UnivRigid | UnivFlexible of bool end +(* XXX: Moved from intf *) module Evar_kinds : sig - type obligation_definition_status = Evar_kinds.obligation_definition_status = - | Define of bool - | Expand + type obligation_definition_status = + | Define of bool + | Expand - type matching_var_kind = Evar_kinds.matching_var_kind = + type matching_var_kind = | FirstOrderPatVar of Names.Id.t | SecondOrderPatVar of Names.Id.t - type t = Evar_kinds.t = + type t = | ImplicitArg of Globnames.global_reference * (int * Names.Id.t option) * bool (** Force inference *) | BinderType of Names.Name.t @@ -1935,7 +2171,7 @@ sig | ImpossibleCase | MatchingVar of matching_var_kind | VarInstance of Names.Id.t - | SubEvar of Evd.evar + | SubEvar of Constr.existential_key end module Evd : @@ -1952,23 +2188,23 @@ sig module Store : sig - type t = Evd.Store.t + type t val empty : t end module Filter : sig - type t = Evd.Filter.t + type t val repr : t -> bool list option end (** This value defines the refinement of a given {i evar} *) - type evar_body = Evd.evar_body = + type evar_body = | Evar_empty (** given {i evar} was not yet refined *) | Evar_defined of Constr.t (** given {i var} was refined to the indicated term *) (** all the information we have concerning some {i evar} *) - type evar_info = Evd.evar_info = + type evar_info = { evar_concl : Constr.t; evar_hyps : Environ.named_context_val; @@ -1990,21 +2226,33 @@ sig (* evar map *) - type evar_map = Evd.evar_map + type evar_map type open_constr = evar_map * Constr.t + open Util + + module Metaset : Set.S with type elt = Constr.metavariable + type rigid = UState.rigid = | UnivRigid | UnivFlexible of bool - type 'a freelisted = 'a Evd.freelisted = { + type 'a freelisted = { rebus : 'a; - freemetas : Evd.Metaset.t + freemetas : Metaset.t } - type instance_status = Evd.instance_status - type clbinding = Evd.clbinding = + + type instance_constraint = IsSuperType | IsSubType | Conv + + type instance_typing_status = + CoerceToType | TypeNotProcessed | TypeProcessed + + type instance_status = instance_constraint * instance_typing_status + + type clbinding = | Cltyp of Names.Name.t * Constr.t freelisted | Clval of Names.Name.t * (Constr.t freelisted * instance_status) * Constr.t freelisted + val empty : evar_map val from_env : Environ.env -> evar_map val find : evar_map -> Evar.t -> evar_info @@ -2057,7 +2305,7 @@ sig end end - type 'a sigma = 'a Evd.sigma = { + type 'a sigma = { it : 'a ; sigma : evar_map } @@ -2074,11 +2322,8 @@ sig val union_evar_universe_context : UState.t -> UState.t -> UState.t val merge_universe_context : evar_map -> UState.t -> evar_map - type unsolvability_explanation = Evd.unsolvability_explanation = - | SeveralInstancesFound of int - - module Metaset : module type of struct include Evd.Metaset end - with type elt = Constr.metavariable + type unsolvability_explanation = + | SeveralInstancesFound of int (** Return {i ids} of all {i evars} that occur in a given term. *) val evars_of_term : Constr.t -> Evar.Set.t @@ -2100,26 +2345,31 @@ sig val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> Environ.env -> evar_map -> Sorts.family -> evar_map * Sorts.t end +(* XXX: moved from intf *) module Constrexpr : sig - type binder_kind = Constrexpr.binder_kind = + + type binder_kind = | Default of Decl_kinds.binding_kind | Generalized of Decl_kinds.binding_kind * Decl_kinds.binding_kind * bool - type explicitation = Constrexpr.explicitation = + + type explicitation = | ExplByPos of int * Names.Id.t option | ExplByName of Names.Id.t type sign = bool type raw_natural_number = string - type prim_token = Constrexpr.prim_token = - | Numeral of raw_natural_number * sign - | String of string + type prim_token = + | Numeral of raw_natural_number * sign + | String of string + type notation = string type instance_expr = Misctypes.glob_level list type proj_flag = int option - type abstraction_kind = Constrexpr.abstraction_kind = - | AbsLambda - | AbsPi - type cases_pattern_expr_r = Constrexpr.cases_pattern_expr_r = + type abstraction_kind = + | AbsLambda + | AbsPi + + type cases_pattern_expr_r = | CPatAlias of cases_pattern_expr * Names.Id.t | CPatCstr of Libnames.reference * cases_pattern_expr list option * cases_pattern_expr list @@ -2137,7 +2387,7 @@ sig and cases_pattern_notation_substitution = cases_pattern_expr list * cases_pattern_expr list list - and constr_expr_r = Constrexpr.constr_expr_r = + and constr_expr_r = | CRef of Libnames.reference * instance_expr option | CFix of Names.Id.t Loc.located * fix_expr list | CCoFix of Names.Id.t Loc.located * cofix_expr list @@ -2158,7 +2408,7 @@ sig * constr_expr * constr_expr | CHole of Evar_kinds.t option * Misctypes.intro_pattern_naming_expr * Genarg.raw_generic_argument option | CPatVar of Names.Id.t - | CEvar of Glob_term.existential_name * (Names.Id.t * constr_expr) list + | CEvar of Names.Id.t * (Names.Id.t * constr_expr) list | CSort of Misctypes.glob_sort | CCast of constr_expr * constr_expr Misctypes.cast_type | CNotation of notation * constr_notation_substitution @@ -2182,12 +2432,12 @@ sig and cofix_expr = Names.Id.t Loc.located * local_binder_expr list * constr_expr * constr_expr - and recursion_order_expr = Constrexpr.recursion_order_expr = + and recursion_order_expr = | CStructRec | CWfRec of constr_expr | CMeasureRec of constr_expr * constr_expr option - and local_binder_expr = Constrexpr.local_binder_expr = + and local_binder_expr = | CLocalAssum of Names.Name.t Loc.located list * binder_kind * constr_expr | CLocalDef of Names.Name.t Loc.located * constr_expr * constr_expr option | CLocalPattern of (cases_pattern_expr * constr_expr option) Loc.located @@ -2201,12 +2451,11 @@ sig type constr_pattern_expr = constr_expr end - module Genredexpr : sig (** The parsing produces initially a list of [red_atom] *) - type 'a red_atom = 'a Genredexpr.red_atom = + type 'a red_atom = | FBeta | FMatch | FFix @@ -2216,7 +2465,7 @@ sig | FDeltaBut of 'a list (** This list of atoms is immediately converted to a [glob_red_flag] *) - type 'a glob_red_flag = 'a Genredexpr.glob_red_flag = { + type 'a glob_red_flag = { rBeta : bool; rMatch : bool; rFix : bool; @@ -2227,7 +2476,7 @@ sig } (** Generic kinds of reductions *) - type ('a,'b,'c) red_expr_gen = ('a,'b,'c) Genredexpr.red_expr_gen = + type ('a,'b,'c) red_expr_gen = | Red of bool | Hnf | Simpl of 'b glob_red_flag*('b,'c) Util.union Locus.with_occurrences option @@ -2241,7 +2490,7 @@ sig | CbvVm of ('b,'c) Util.union Locus.with_occurrences option | CbvNative of ('b,'c) Util.union Locus.with_occurrences option - type ('a,'b,'c) may_eval = ('a,'b,'c) Genredexpr.may_eval = + type ('a,'b,'c) may_eval = | ConstrTerm of 'a | ConstrEval of ('a,'b,'c) red_expr_gen * 'a | ConstrContext of Names.Id.t Loc.located * 'a @@ -2253,12 +2502,14 @@ sig type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen end +(* XXX: end of moved from intf *) + module EConstr : sig - type t = EConstr.t + type t type constr = t type types = t - type unsafe_judgment = EConstr.unsafe_judgment + type unsafe_judgment = (constr, types) Environ.punsafe_judgment type named_declaration = (constr, types) Context.Named.Declaration.pt type named_context = (constr, types) Context.Named.pt type rel_context = (constr, types) Context.Rel.pt @@ -2266,7 +2517,7 @@ sig type existential = constr Constr.pexistential module ESorts : sig - type t = EConstr.ESorts.t + type t (** Type of sorts up-to universe unification. Essentially a wrapper around Sorts.t so that normalization is ensured statically. *) @@ -2281,7 +2532,7 @@ sig module EInstance : sig - type t = EConstr.EInstance.t + type t (** Type of universe instances up-to universe unification. Similar to {ESorts.t} for {Univ.Instance.t}. *) @@ -2424,8 +2675,14 @@ end (* XXX: Located manually from intf *) module Pattern : sig - type case_info_pattern = Pattern.case_info_pattern - type constr_pattern = Pattern.constr_pattern = + + type case_info_pattern = + { cip_style : Misctypes.case_style; + cip_ind : Names.inductive option; + cip_ind_tags : bool list option; (** indicates LetIn/Lambda in arity *) + cip_extensible : bool (** does this match end with _ => _ ? *) } + + type constr_pattern = | PRef of Globnames.global_reference | PVar of Names.Id.t | PEvar of Evar.t * constr_pattern array @@ -2567,7 +2824,7 @@ sig type lazy_msg = unit -> Pp.std_ppcmds module Info : sig - type tree = Proofview_monad.Info.tree + type tree end end @@ -2603,7 +2860,11 @@ sig val clear_hyps_in_evi : Environ.env -> Evd.evar_map ref -> Environ.named_context_val -> EConstr.types -> Names.Id.Set.t -> Environ.named_context_val * EConstr.types - exception ClearDependencyError of Names.Id.t * Evarutil.clear_dependency_error + type clear_dependency_error = + | OccurHypInSimpleClause of Names.Id.t option + | EvarTypingBreak of Constr.existential + + exception ClearDependencyError of Names.Id.t * clear_dependency_error val undefined_evars_of_term : Evd.evar_map -> EConstr.constr -> Evar.Set.t val e_new_evar : Environ.env -> Evd.evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t -> @@ -2621,15 +2882,16 @@ end module Proofview : sig - type proofview = Proofview.proofview - type entry = Proofview.entry - type +'a tactic = 'a Proofview.tactic - type telescope = Proofview.telescope = + type proofview + type entry + type +'a tactic + type telescope = | TNil of Evd.evar_map | TCons of Environ.env * Evd.evar_map * EConstr.types * (Evd.evar_map -> EConstr.constr -> telescope) + module NonLogical : sig - type +'a t = 'a Proofview.NonLogical.t + type +'a t val make : (unit -> 'a) -> 'a t val return : 'a -> 'a t val ( >> ) : unit t -> 'a t -> 'a t @@ -2640,7 +2902,7 @@ sig val print_notice : Pp.std_ppcmds -> unit t val print_info : Pp.std_ppcmds -> unit t val run : 'a t -> 'a - type 'a ref = 'a Proofview.NonLogical.ref + type 'a ref val ref : 'a -> 'a ref t val ( := ) : 'a ref -> 'a -> unit t val ( ! ) : 'a ref -> 'a t @@ -2693,7 +2955,7 @@ sig module Goal : sig - type 'a t = 'a Proofview.Goal.t + type 'a t val enter : ([ `LZ ] t -> unit tactic) -> unit tactic val hyps : 'a t -> EConstr.named_context val nf_enter : ([ `NF ] t -> unit tactic) -> unit tactic @@ -2734,7 +2996,7 @@ end module Ftactic : sig - type +'a focus = 'a Ftactic.focus + type +'a focus type +'a t = 'a focus Proofview.tactic val return : 'a -> 'a t val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic @@ -2760,9 +3022,9 @@ module Geninterp : sig module Val : sig - type 'a typ = 'a Geninterp.Val.typ - type t = Geninterp.Val.t = Dyn : 'a typ * 'a -> t - type 'a tag = 'a Geninterp.Val.tag = + type 'a typ + type t = Dyn : 'a typ * 'a -> t + type 'a tag = | Base : 'a typ -> 'a tag | List : 'a tag -> 'a list tag | Opt : 'a tag -> 'a option tag @@ -2778,8 +3040,8 @@ sig end module TacStore : sig - type t = Geninterp.TacStore.t - type 'a field = 'a Geninterp.TacStore.field + type t + type 'a field val empty : t val field : unit -> 'a field val get : t -> 'a field -> 'a option @@ -2787,9 +3049,10 @@ sig val remove : t -> 'a field -> t val merge : t -> t -> t end - type interp_sign = Geninterp.interp_sign = - {lfun : Val.t Names.Id.Map.t; - extra : TacStore.t } + type interp_sign = { + lfun : Val.t Names.Id.Map.t; + extra : TacStore.t + } type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t val register_interp0 : ('raw, 'glb, 'top) Genarg.genarg_type -> ('glb, Val.t) interp_fun -> unit @@ -2801,12 +3064,12 @@ end (* XXX: Located manually from intf *) module Glob_term : sig - type cases_pattern_r = Glob_term.cases_pattern_r = + type cases_pattern_r = | PatVar of Names.Name.t | PatCstr of Names.constructor * cases_pattern list * Names.Name.t and cases_pattern = cases_pattern_r CAst.t type existential_name = Names.Id.t - type glob_constr_r = Glob_term.glob_constr_r = + type glob_constr_r = | GRef of Globnames.global_reference * Misctypes.glob_level list option (** An identifier that represents a reference to an object defined either in the (global) environment or in the (local) context. *) @@ -2832,14 +3095,14 @@ sig and glob_decl = Names.Name.t * Decl_kinds.binding_kind * glob_constr option * glob_constr - and fix_recursion_order = Glob_term.fix_recursion_order = - | GStructRec - | GWfRec of glob_constr - | GMeasureRec of glob_constr * glob_constr option + and fix_recursion_order = + | GStructRec + | GWfRec of glob_constr + | GMeasureRec of glob_constr * glob_constr option - and fix_kind = Glob_term.fix_kind = - | GFix of ((int option * fix_recursion_order) array * int) - | GCoFix of int + and fix_kind = + | GFix of ((int option * fix_recursion_order) array * int) + | GCoFix of int and predicate_pattern = Names.Name.t * (Names.inductive * Names.Name.t list) Loc.located option @@ -2855,11 +3118,11 @@ sig of its free variables. Intended for use when these variables are taken from the Ltac environment. *) - type closure = Glob_term.closure = { + type closure = { idents : Names.Id.t Names.Id.Map.t; typed : Pattern.constr_under_binders Names.Id.Map.t ; untyped: closed_glob_constr Names.Id.Map.t } - and closed_glob_constr = Glob_term.closed_glob_constr = { + and closed_glob_constr = { closure: closure; term: glob_constr } @@ -2884,11 +3147,12 @@ end module Notation_term : sig type scope_name = string - type notation_var_instance_type = Notation_term.notation_var_instance_type = + type notation_var_instance_type = | NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList - type tmp_scope_name = Notation_term.tmp_scope_name + type tmp_scope_name = scope_name + type subscopes = tmp_scope_name option * scope_name list - type notation_constr = Notation_term.notation_constr = + type notation_constr = | NRef of Globnames.global_reference | NVar of Names.Id.t | NApp of notation_constr * notation_constr list @@ -2927,6 +3191,8 @@ sig type or_and_intro_pattern = delayed_open_constr Misctypes.or_and_intro_pattern_expr Loc.located end +(* XXX: end of moved from intf *) + (************************************************************************) (* End of modules from engine/ *) (************************************************************************) @@ -2950,29 +3216,32 @@ end module Pretype_errors : sig - type unification_error = Pretype_errors.unification_error - type subterm_unification_error = Pretype_errors.subterm_unification_error - type pretype_error = Pretype_errors.pretype_error = - | CantFindCaseType of EConstr.constr - | ActualTypeNotCoercible of EConstr.unsafe_judgment * EConstr.types * unification_error - | UnifOccurCheck of Evar.t * EConstr.constr - | UnsolvableImplicit of Evar.t * Evd.unsolvability_explanation option - | CannotUnify of EConstr.constr * EConstr.constr * unification_error option - | CannotUnifyLocal of EConstr.constr * EConstr.constr * EConstr.constr - | CannotUnifyBindingType of EConstr.constr * EConstr.constr - | CannotGeneralize of EConstr.constr - | NoOccurrenceFound of EConstr.constr * Names.Id.t option - | CannotFindWellTypedAbstraction of EConstr.constr * EConstr.constr list * (Environ.env * Pretype_errors.type_error) option - | WrongAbstractionType of Names.Name.t * EConstr.constr * EConstr.types * EConstr.types - | AbstractionOverMeta of Names.Name.t * Names.Name.t - | NonLinearUnification of Names.Name.t * EConstr.constr - | VarNotFound of Names.Id.t - | UnexpectedType of EConstr.constr * EConstr.constr - | NotProduct of EConstr.constr - | TypingError of Pretype_errors.type_error - | CannotUnifyOccurrences of subterm_unification_error - | UnsatisfiableConstraints of - (Evar.t * Evar_kinds.t) option * Evar.Set.t option + type unification_error + type subterm_unification_error + + type type_error = (EConstr.t, EConstr.types) Type_errors.ptype_error + + type pretype_error = + | CantFindCaseType of EConstr.constr + | ActualTypeNotCoercible of EConstr.unsafe_judgment * EConstr.types * unification_error + | UnifOccurCheck of Evar.t * EConstr.constr + | UnsolvableImplicit of Evar.t * Evd.unsolvability_explanation option + | CannotUnify of EConstr.constr * EConstr.constr * unification_error option + | CannotUnifyLocal of EConstr.constr * EConstr.constr * EConstr.constr + | CannotUnifyBindingType of EConstr.constr * EConstr.constr + | CannotGeneralize of EConstr.constr + | NoOccurrenceFound of EConstr.constr * Names.Id.t option + | CannotFindWellTypedAbstraction of EConstr.constr * EConstr.constr list * (Environ.env * type_error) option + | WrongAbstractionType of Names.Name.t * EConstr.constr * EConstr.types * EConstr.types + | AbstractionOverMeta of Names.Name.t * Names.Name.t + | NonLinearUnification of Names.Name.t * EConstr.constr + | VarNotFound of Names.Id.t + | UnexpectedType of EConstr.constr * EConstr.constr + | NotProduct of EConstr.constr + | TypingError of type_error + | CannotUnifyOccurrences of subterm_unification_error + | UnsatisfiableConstraints of + (Evar.t * Evar_kinds.t) option * Evar.Set.t option exception PretypeError of Environ.env * Evd.evar_map * pretype_error val error_var_not_found : ?loc:Loc.t -> Names.Id.t -> 'b @@ -2989,7 +3258,7 @@ sig Evd.evar_map -> EConstr.constr -> EConstr.constr * EConstr.constr list type e_reduction_function = Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.constr - type state = Reductionops.state + type state val clos_whd_flags : CClosure.RedFlags.reds -> reduction_function val nf_beta : local_reduction_function @@ -3017,22 +3286,22 @@ sig val pr_state : state -> Pp.std_ppcmds module Stack : sig - type 'a t = 'a Reductionops.Stack.t + type 'a t val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds end module Cst_stack : sig - type t = Reductionops.Cst_stack.t + type t val pr : t -> Pp.std_ppcmds end end module Inductiveops : sig - type inductive_family = Inductiveops.inductive_family - type inductive_type = Inductiveops.inductive_type = + type inductive_family + type inductive_type = | IndType of inductive_family * EConstr.constr list - type constructor_summary = Inductiveops.constructor_summary = + type constructor_summary = { cs_cstr : Term.pconstructor; cs_params : Constr.t list; @@ -3063,8 +3332,8 @@ end module Impargs : sig - type implicit_status = Impargs.implicit_status - type implicit_side_condition = Impargs.implicit_side_condition + type implicit_status + type implicit_side_condition type implicits_list = implicit_side_condition * implicit_status list type manual_explicitation = Constrexpr.explicitation * (bool * bool * bool) type manual_implicits = manual_explicitation list @@ -3104,12 +3373,14 @@ end module Recordops : sig - type cs_pattern = Recordops.cs_pattern = + + type cs_pattern = | Const_cs of Globnames.global_reference | Prod_cs | Sort_cs of Sorts.family | Default_cs - type obj_typ = Recordops.obj_typ = { + + type obj_typ = { o_DEF : Constr.t; o_CTX : Univ.AUContext.t; o_INJ : int option; (** position of trivial argument *) @@ -3117,6 +3388,7 @@ sig o_TPARAMS : Constr.t list; (** ordered *) o_NPARAMS : int; o_TCOMPS : Constr.t list } + val lookup_projections : Names.inductive -> Names.Constant.t option list val lookup_canonical_conversion : (Globnames.global_reference * cs_pattern) -> Constr.t * obj_typ val find_projection_nparams : Globnames.global_reference -> int @@ -3151,13 +3423,6 @@ sig val map_cast_type : ('a -> 'b) -> 'a Misctypes.cast_type -> 'b Misctypes.cast_type end -module Stm : -sig - type state = Stm.state - val state_of_id : - Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ] -end - module Glob_ops : sig val map_glob_constr_left_to_right : (Glob_term.glob_constr -> Glob_term.glob_constr) -> Glob_term.glob_constr -> Glob_term.glob_constr @@ -3233,21 +3498,145 @@ sig end (* XXX: Located manually from intf *) +module Tok : +sig + + type t = + | KEYWORD of string + | PATTERNIDENT of string + | IDENT of string + | FIELD of string + | INT of string + | STRING of string + | LEFTQMARK + | BULLET of string + | EOI + +end + +module CLexer : +sig + val add_keyword : string -> unit + val remove_keyword : string -> unit + val is_keyword : string -> bool + val keywords : unit -> CString.Set.t + + type keyword_state + val set_keyword_state : keyword_state -> unit + val get_keyword_state : unit -> keyword_state + + val check_ident : string -> unit + val terminal : string -> Tok.t + + include Grammar.GLexerType with type te = Tok.t +end + +module Extend : +sig + + type gram_assoc = NonA | RightA | LeftA + + type gram_position = + | First + | Last + | Before of string + | After of string + | Level of string + + type production_level = + | NextLevel + | NumLevel of int + + type 'a entry = 'a Grammar.GMake(CLexer).Entry.e + + type 'a user_symbol = + | Ulist1 of 'a user_symbol + | Ulist1sep of 'a user_symbol * string + | Ulist0 of 'a user_symbol + | Ulist0sep of 'a user_symbol * string + | Uopt of 'a user_symbol + | Uentry of 'a + | Uentryl of 'a * int + + type ('self, 'a) symbol = + | Atoken : Tok.t -> ('self, string) symbol + | Alist1 : ('self, 'a) symbol -> ('self, 'a list) symbol + | Alist1sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol + | Alist0 : ('self, 'a) symbol -> ('self, 'a list) symbol + | Alist0sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol + | Aopt : ('self, 'a) symbol -> ('self, 'a option) symbol + | Aself : ('self, 'self) symbol + | Anext : ('self, 'self) symbol + | Aentry : 'a entry -> ('self, 'a) symbol + | Aentryl : 'a entry * int -> ('self, 'a) symbol + | Arules : 'a rules list -> ('self, 'a) symbol + + and ('self, _, 'r) rule = + | Stop : ('self, 'r, 'r) rule + | Next : ('self, 'a, 'r) rule * ('self, 'b) symbol -> ('self, 'b -> 'a, 'r) rule + + and ('a, 'r) norec_rule = { norec_rule : 's. ('s, 'a, 'r) rule } + + and 'a rules = + | Rules : ('act, Loc.t -> 'a) norec_rule * 'act -> 'a rules + + type ('lev,'pos) constr_entry_key_gen = + | ETName | ETReference | ETBigint + | ETBinder of bool + | ETConstr of ('lev * 'pos) + | ETPattern + | ETOther of string * string + | ETConstrList of ('lev * 'pos) * Tok.t list + | ETBinderList of bool * Tok.t list + + type side = Left | Right + + type production_position = + | BorderProd of side * gram_assoc option + | InternalProd + + type constr_prod_entry_key = + (production_level,production_position) constr_entry_key_gen + + type simple_constr_prod_entry_key = + (production_level,unit) constr_entry_key_gen + + type 'a production_rule = + | Rule : ('a, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule + + type 'a single_extend_statment = + string option * + (** Level *) + gram_assoc option * + (** Associativity *) + 'a production_rule list + (** Symbol list with the interpretation function *) + + type 'a extend_statment = + gram_position option * + 'a single_extend_statment list +end + +(* XXX: Located manually from intf *) module Vernacexpr : sig + open Misctypes + open Constrexpr + open Libnames + type instance_flag = bool option type coercion_flag = bool type inductive_flag = Decl_kinds.recursivity_kind type lname = Names.Name.t Loc.located type lident = Names.Id.t Loc.located - type opacity_flag = Vernacexpr.opacity_flag = + type opacity_flag = | Opaque of lident list option | Transparent type locality_flag = bool - type inductive_kind = Vernacexpr.inductive_kind = + type inductive_kind = | Inductive_kw | CoInductive | Variant | Record | Structure | Class of bool - type vernac_type = Vernacexpr.vernac_type = + type vernac_type = | VtStartProof of vernac_start | VtSideff of vernac_sideff_type | VtQed of vernac_qed_type @@ -3256,92 +3645,119 @@ sig | VtQuery of vernac_part_of_script * Feedback.route_id | VtStm of vernac_control * vernac_part_of_script | VtUnknown - and vernac_qed_type = Vernacexpr.vernac_qed_type = - | VtKeep - | VtKeepAsAxiom - | VtDrop + and vernac_qed_type = + | VtKeep + | VtKeepAsAxiom + | VtDrop and vernac_start = string * opacity_guarantee * Names.Id.t list and vernac_sideff_type = Names.Id.t list and vernac_part_of_script = bool - and vernac_control = Vernacexpr.vernac_control = - | VtWait - | VtJoinDocument - | VtBack of Stateid.t - and opacity_guarantee = Vernacexpr.opacity_guarantee = - | GuaranteesOpacity - | Doesn'tGuaranteeOpacity - and proof_step = Vernacexpr.proof_step = { - parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ]; - proof_block_detection : proof_block_name option - } + and vernac_control = + | VtWait + | VtJoinDocument + | VtBack of Stateid.t + and opacity_guarantee = + | GuaranteesOpacity + | Doesn'tGuaranteeOpacity + and proof_step = { + parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ]; + proof_block_detection : proof_block_name option + } and solving_tac = bool and anon_abstracting_tac = bool and proof_block_name = string - type vernac_when = Vernacexpr.vernac_when = - | VtNow - | VtLater + + type vernac_when = + | VtNow + | VtLater + type verbose_flag = bool type obsolete_locality = bool - type lstring = Vernacexpr.lstring + type lstring type 'a with_coercion = coercion_flag * 'a type scope_name = string type decl_notation = lstring * Constrexpr.constr_expr * scope_name option type constructor_expr = (lident * Constrexpr.constr_expr) with_coercion type 'a with_notation = 'a * decl_notation list - type local_decl_expr = Vernacexpr.local_decl_expr = + + type local_decl_expr = | AssumExpr of lname * Constrexpr.constr_expr | DefExpr of lname * Constrexpr.constr_expr * Constrexpr.constr_expr option + type 'a with_priority = 'a * int option type 'a with_instance = instance_flag * 'a - type constructor_list_or_record_decl_expr = Vernacexpr.constructor_list_or_record_decl_expr = + type constructor_list_or_record_decl_expr = | Constructors of constructor_expr list | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list + type plident = lident * lident list option + type inductive_expr = plident with_coercion * Constrexpr.local_binder_expr list * Constrexpr.constr_expr option * inductive_kind * constructor_list_or_record_decl_expr - type syntax_modifier = Vernacexpr.syntax_modifier - type class_rawexpr = Vernacexpr.class_rawexpr - type definition_expr = Vernacexpr.definition_expr - type proof_expr = Vernacexpr.proof_expr - type proof_end = Vernacexpr.proof_end = + type syntax_modifier = + | SetItemLevel of string list * Extend.production_level + | SetLevel of int + | SetAssoc of Extend.gram_assoc + | SetEntryType of string * Extend.simple_constr_prod_entry_key + | SetOnlyParsing + | SetOnlyPrinting + | SetCompatVersion of Flags.compat_version + | SetFormat of string * string Loc.located + + type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation + + type definition_expr = + | ProveBody of local_binder_expr list * constr_expr + | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr + * constr_expr option + type proof_expr = + plident option * (local_binder_expr list * constr_expr) + + type proof_end = | Admitted | Proved of opacity_flag * lident option + type fixpoint_expr = plident * (Names.Id.t Loc.located option * Constrexpr.recursion_order_expr) * Constrexpr.local_binder_expr list * Constrexpr.constr_expr * Constrexpr.constr_expr option - type cofixpoint_expr = Vernacexpr.cofixpoint_expr - type scheme = Vernacexpr.scheme - type section_subset_expr = Vernacexpr.section_subset_expr - type module_binder = Vernacexpr.module_binder - type vernac_argument_status = Vernacexpr.vernac_argument_status - type vernac_implicit_status = Vernacexpr.vernac_implicit_status - type module_ast_inl = Vernacexpr.module_ast_inl + + type cofixpoint_expr + + type scheme + + type section_subset_expr + + type module_binder + + type vernac_argument_status + type vernac_implicit_status + type module_ast_inl type extend_name = string * int - type simple_binder = Vernacexpr.simple_binder - type option_value = Vernacexpr.option_value - type showable = Vernacexpr.showable - type bullet = Vernacexpr.bullet - type stm_vernac = Vernacexpr.stm_vernac - type comment = Vernacexpr.comment - type register_kind = Vernacexpr.register_kind - type locatable = Vernacexpr.locatable - type search_restriction = Vernacexpr.search_restriction - type searchable = Vernacexpr.searchable - type printable = Vernacexpr.printable - type option_ref_value = Vernacexpr.option_ref_value - type onlyparsing_flag = Vernacexpr.onlyparsing_flag - type reference_or_constr = Vernacexpr.reference_or_constr - - type hint_mode = Vernacexpr.hint_mode - - type 'a hint_info_gen = 'a Vernacexpr.hint_info_gen = + type simple_binder + type option_value + type showable + type bullet + type stm_vernac + type comment + type register_kind + type locatable + type search_restriction + type searchable + type printable + type option_ref_value + type onlyparsing_flag + type reference_or_constr + + type hint_mode + + type 'a hint_info_gen = { hint_priority : int option; hint_pattern : 'a option } type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen - type hints_expr = Vernacexpr.hints_expr = - | HintsResolve of (Vernacexpr.hint_info_expr * bool * reference_or_constr) list + type hints_expr = + | HintsResolve of (hint_info_expr * bool * reference_or_constr) list | HintsImmediate of reference_or_constr list | HintsUnfold of Libnames.reference list | HintsTransparency of Libnames.reference list * bool @@ -3349,16 +3765,16 @@ sig | HintsConstructors of Libnames.reference list | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument - type 'a module_signature = 'a Vernacexpr.module_signature = + type 'a module_signature = | Enforce of 'a (** ... : T *) | Check of 'a list (** ... <: T1 <: T2, possibly empty *) - type inline = Vernacexpr.inline = + type inline = | NoInline | DefaultInline | InlineAt of int - type vernac_expr = Vernacexpr.vernac_expr = + type vernac_expr = | VernacLoad of verbose_flag * string | VernacTime of vernac_expr Loc.located | VernacRedirect of string * vernac_expr Loc.located @@ -3490,7 +3906,7 @@ sig | VernacProgram of vernac_expr | VernacPolymorphic of bool * vernac_expr | VernacLocal of bool * vernac_expr - and goal_selector = Vernacexpr.goal_selector = + and goal_selector = | SelectNth of int | SelectList of (int * int) list | SelectId of Names.Id.t @@ -3500,10 +3916,11 @@ sig plident * Constrexpr.local_binder_expr list * Constrexpr.constr_expr option * constructor_expr list end +(* XXX: end manual intf move *) module Typeclasses : sig - type typeclass = Typeclasses.typeclass = { + type typeclass = { cl_univs : Univ.AUContext.t; cl_impl : Globnames.global_reference; cl_context : (Globnames.global_reference * bool) option list * Context.Rel.t; @@ -3513,9 +3930,11 @@ sig cl_strict : bool; cl_unique : bool; } - and direction = Typeclasses.direction - type instance = Typeclasses.instance + and direction + + type instance type evar_filter = Evar.t -> Evar_kinds.t -> bool + val resolve_typeclasses : ?fast_path:bool -> ?filter:evar_filter -> ?unique:bool -> ?split:bool -> ?fail:bool -> Environ.env -> Evd.evar_map -> Evd.evar_map val set_resolvable : Evd.Store.t -> bool -> Evd.Store.t @@ -3529,9 +3948,9 @@ end module Classops : sig - type coe_index = Classops.coe_index + type coe_index type inheritance_path = coe_index list - type cl_index = Classops.cl_index + type cl_index val hide_coercion : Globnames.global_reference -> int option val lookup_path_to_sort_from : Environ.env -> Evd.evar_map -> EConstr.types -> @@ -3565,13 +3984,14 @@ end module Pretyping : sig - type typing_constraint = Pretyping.typing_constraint = - | OfType of EConstr.types - | IsType - | WithoutTypeConstraint + type typing_constraint = + | OfType of EConstr.types + | IsType + | WithoutTypeConstraint type inference_hook = Environ.env -> Evd.evar_map -> Evar.t -> Evd.evar_map * EConstr.constr - type inference_flags = Pretyping.inference_flags = { + + type inference_flags = { use_typeclasses : bool; solve_unification_constraints : bool; use_hook : inference_hook option; @@ -3606,29 +4026,28 @@ end module Unification : sig - type core_unify_flags = Unification.core_unify_flags = - { - modulo_conv_on_closed_terms : Names.transparent_state option; - use_metas_eagerly_in_conv_on_closed_terms : bool; - use_evars_eagerly_in_conv_on_closed_terms : bool; - modulo_delta : Names.transparent_state; - modulo_delta_types : Names.transparent_state; - check_applied_meta_types : bool; - use_pattern_unification : bool; - use_meta_bound_pattern_unification : bool; - frozen_evars : Evar.Set.t; - restrict_conv_on_strict_subterms : bool; - modulo_betaiota : bool; - modulo_eta : bool; - } - type unify_flags = Unification.unify_flags = - { - core_unify_flags : core_unify_flags; - merge_unify_flags : core_unify_flags; - subterm_unify_flags : core_unify_flags; - allow_K_in_toplevel_higher_order_unification : bool; - resolve_evars : bool - } + type core_unify_flags = { + modulo_conv_on_closed_terms : Names.transparent_state option; + use_metas_eagerly_in_conv_on_closed_terms : bool; + use_evars_eagerly_in_conv_on_closed_terms : bool; + modulo_delta : Names.transparent_state; + modulo_delta_types : Names.transparent_state; + check_applied_meta_types : bool; + use_pattern_unification : bool; + use_meta_bound_pattern_unification : bool; + frozen_evars : Evar.Set.t; + restrict_conv_on_strict_subterms : bool; + modulo_betaiota : bool; + modulo_eta : bool; + } + type unify_flags = + { + core_unify_flags : core_unify_flags; + merge_unify_flags : core_unify_flags; + subterm_unify_flags : core_unify_flags; + allow_K_in_toplevel_higher_order_unification : bool; + resolve_evars : bool + } val default_no_delta_unify_flags : unit -> unify_flags val w_unify : Environ.env -> Evd.evar_map -> Reduction.conv_pb -> ?flags:unify_flags -> EConstr.constr -> EConstr.constr -> Evd.evar_map val elim_flags : unit -> unify_flags @@ -3644,6 +4063,41 @@ end (* Modules from interp/ *) (************************************************************************) +module Genintern : +sig + open Genarg + + module Store : Store.S + + type glob_sign = { + ltacvars : Names.Id.Set.t; + genv : Environ.env; + extra : Store.t; + } + + val empty_glob_sign : Environ.env -> glob_sign + + type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb + + + val generic_intern : (raw_generic_argument, glob_generic_argument) intern_fun + + type 'glb subst_fun = Mod_subst.substitution -> 'glb -> 'glb + val generic_substitute : Genarg.glob_generic_argument subst_fun + + type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Names.Id.Map.t -> 'glb -> 'glb + + val register_intern0 : ('raw, 'glb, 'top) genarg_type -> + ('raw, 'glb) intern_fun -> unit + + val register_subst0 : ('raw, 'glb, 'top) genarg_type -> + 'glb subst_fun -> unit + + val register_ntn_subst0 : ('raw, 'glb, 'top) genarg_type -> + 'glb ntn_subst_fun -> unit + +end + module Stdarg : sig val loc_of_or_by_notation : ('a -> Loc.t option) -> 'a Misctypes.or_by_notation -> Loc.t option @@ -3713,10 +4167,12 @@ end module Ppextend : sig + type precedence = int - type parenRelation = Ppextend.parenRelation = - | L | E | Any | Prec of precedence + type parenRelation = + | L | E | Any | Prec of precedence type tolerability = precedence * parenRelation + end module Notation : @@ -3768,13 +4224,15 @@ end module Constrintern : sig - type ltac_sign = Constrintern.ltac_sign = { - ltac_vars : Names.Id.Set.t; - ltac_bound : Names.Id.Set.t; - ltac_extra : Genintern.Store.t; - } - type var_internalization_data = Constrintern.var_internalization_data - type var_internalization_type = Constrintern.var_internalization_type = + type ltac_sign = { + ltac_vars : Names.Id.Set.t; + ltac_bound : Names.Id.Set.t; + ltac_extra : Genintern.Store.t; + } + + type var_internalization_data + + type var_internalization_type = | Inductive of Names.Id.t list * bool | Recursive | Method @@ -3828,18 +4286,24 @@ end module Declare : sig - type internal_flag = Declare.internal_flag = + type internal_flag = | UserAutomaticRequest | InternalTacticRequest | UserIndividualRequest + type constant_declaration = Safe_typing.private_constants Entries.constant_entry * Decl_kinds.logical_kind - type section_variable_entry = Declare.section_variable_entry = + + type section_variable_entry = | SectionLocalDef of Safe_typing.private_constants Entries.definition_entry | SectionLocalAssum of Term.types Univ.in_universe_context_set * Decl_kinds.polymorphic * bool + type variable_declaration = Names.DirPath.t * section_variable_entry * Decl_kinds.logical_kind + val declare_constant : ?internal:internal_flag -> ?local:bool -> Names.Id.t -> ?export_seff:bool -> constant_declaration -> Names.Constant.t + val declare_universe_context : Decl_kinds.polymorphic -> Univ.ContextSet.t -> unit + val declare_definition : ?internal:internal_flag -> ?opaque:bool -> ?kind:Decl_kinds.definition_object_kind -> ?local:bool -> ?poly:Decl_kinds.polymorphic -> Names.Id.t -> ?types:Constr.t -> @@ -3922,7 +4386,7 @@ end module Proof_type : sig - type prim_rule = Proof_type.prim_rule = + type prim_rule = | Cut of bool * bool * Names.Id.t * Term.types | Refine of Constr.t @@ -3931,7 +4395,7 @@ end module Logic : sig - type refiner_error = Logic.refiner_error = + type refiner_error = | BadType of Constr.t * Constr.t * Constr.t | UnresolvedBindings of Names.Name.t list | CannotApply of Constr.t * Constr.t @@ -3953,8 +4417,9 @@ end module Proof : sig - type proof = Proof.proof - type 'a focus_kind = 'a Proof.focus_kind + type proof + type 'a focus_kind + val run_tactic : Environ.env -> unit Proofview.tactic -> proof -> proof * (bool * Proofview_monad.Info.tree) val unshelve : proof -> proof @@ -3975,28 +4440,31 @@ end module Proof_global : sig - type proof_mode = Proof_global.proof_mode = { + type proof_mode = { name : string; set : unit -> unit ; reset : unit -> unit } type proof_universes = UState.t * Universes.universe_binders option - type proof_object = Proof_global.proof_object = { - id : Names.Id.t; - entries : Safe_typing.private_constants Entries.definition_entry list; - persistence : Decl_kinds.goal_kind; - universes: proof_universes; - } - type proof_ending = Proof_global.proof_ending = + type proof_object = { + id : Names.Id.t; + entries : Safe_typing.private_constants Entries.definition_entry list; + persistence : Decl_kinds.goal_kind; + universes: proof_universes; + } + + type proof_ending = | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes | Proved of Vernacexpr.opacity_flag * Vernacexpr.lident option * proof_object - type proof_terminator = Proof_global.proof_terminator - type lemma_possible_guards = Proof_global.lemma_possible_guards - type universe_binders = Proof_global.universe_binders + + type proof_terminator + type lemma_possible_guards + type universe_binders type closed_proof = proof_object * proof_terminator + val make_terminator : (proof_ending -> unit) -> proof_terminator val start_dependent_proof : Names.Id.t -> ?pl:universe_binders -> Decl_kinds.goal_kind -> @@ -4155,22 +4623,25 @@ end module Clenv : sig - type hole = Clenv.hole = { - hole_evar : EConstr.constr; - hole_type : EConstr.types; - hole_deps : bool; - hole_name : Names.Name.t; - } - type clause = Clenv.clause = { - cl_holes : hole list; - cl_concl : EConstr.types; - } + + type hole = { + hole_evar : EConstr.constr; + hole_type : EConstr.types; + hole_deps : bool; + hole_name : Names.Name.t; + } + + type clause = { + cl_holes : hole list; + cl_concl : EConstr.types; + } + val make_evar_clause : Environ.env -> Evd.evar_map -> ?len:int -> EConstr.types -> (Evd.evar_map * clause) val solve_evar_clause : Environ.env -> Evd.evar_map -> bool -> clause -> EConstr.constr Misctypes.bindings -> Evd.evar_map - type clausenv = Clenv.clausenv - val pr_clenv : Clenv.clausenv -> Pp.std_ppcmds + type clausenv + val pr_clenv : clausenv -> Pp.std_ppcmds end (************************************************************************) @@ -4181,7 +4652,179 @@ end (* Modules from parsing/ *) (************************************************************************) +module Pcoq : +sig + + open Loc + open Names + open Extend + open Vernacexpr + open Genarg + open Constrexpr + open Libnames + open Misctypes + open Genredexpr + + module Gram : sig + include Grammar.S with type te = Tok.t + + type 'a entry = 'a Entry.e + type internal_entry = Tok.t Gramext.g_entry + type symbol = Tok.t Gramext.g_symbol + type action = Gramext.g_action + type production_rule = symbol list * action + type single_extend_statment = + string option * Gramext.g_assoc option * production_rule list + type extend_statment = + Gramext.position option * single_extend_statment list + + type coq_parsable + + val parsable : ?file:string -> char Stream.t -> coq_parsable + val action : 'a -> action + val entry_create : string -> 'a entry + val entry_parse : 'a entry -> coq_parsable -> 'a + val entry_print : Format.formatter -> 'a entry -> unit + val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b + (* Apparently not used *) + val srules' : production_rule list -> symbol + val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a + + end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e + + val parse_string : 'a Gram.entry -> string -> 'a + val eoi_entry : 'a Gram.entry -> 'a Gram.entry + val map_entry : ('a -> 'b) -> 'a Gram.entry -> 'b Gram.entry + + type gram_universe + + val uprim : gram_universe + val uconstr : gram_universe + val utactic : gram_universe + val uvernac : gram_universe + + val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry -> unit + + val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry + + val create_generic_entry : gram_universe -> string -> + ('a, rlevel) abstract_argument_type -> 'a Gram.entry + + module Prim : + sig + open Names + open Libnames + val preident : string Gram.entry + val ident : Id.t Gram.entry + val name : Name.t located Gram.entry + val identref : Id.t located Gram.entry + val pidentref : (Id.t located * (Id.t located list) option) Gram.entry + val pattern_ident : Id.t Gram.entry + val pattern_identref : Id.t located Gram.entry + val base_ident : Id.t Gram.entry + val natural : int Gram.entry + val bigint : Constrexpr.raw_natural_number Gram.entry + val integer : int Gram.entry + val string : string Gram.entry + val lstring : string located Gram.entry + val qualid : qualid located Gram.entry + val fullyqualid : Id.t list located Gram.entry + val reference : reference Gram.entry + val by_notation : (string * string option) Loc.located Gram.entry + val smart_global : reference or_by_notation Gram.entry + val dirpath : DirPath.t Gram.entry + val ne_string : string Gram.entry + val ne_lstring : string located Gram.entry + val var : Id.t located Gram.entry + end + + module Constr : + sig + val constr : constr_expr Gram.entry + val constr_eoi : constr_expr Gram.entry + val lconstr : constr_expr Gram.entry + val binder_constr : constr_expr Gram.entry + val operconstr : constr_expr Gram.entry + val ident : Id.t Gram.entry + val global : reference Gram.entry + val universe_level : glob_level Gram.entry + val sort : glob_sort Gram.entry + val pattern : cases_pattern_expr Gram.entry + val constr_pattern : constr_expr Gram.entry + val lconstr_pattern : constr_expr Gram.entry + val closed_binder : local_binder_expr list Gram.entry + val binder : local_binder_expr list Gram.entry (* closed_binder or variable *) + val binders : local_binder_expr list Gram.entry (* list of binder *) + val open_binders : local_binder_expr list Gram.entry + val binders_fixannot : (local_binder_expr list * (Id.t located option * recursion_order_expr)) Gram.entry + val typeclass_constraint : (Name.t located * bool * constr_expr) Gram.entry + val record_declaration : constr_expr Gram.entry + val appl_arg : (constr_expr * explicitation located option) Gram.entry + end + + module Vernac_ : + sig + val gallina : vernac_expr Gram.entry + val gallina_ext : vernac_expr Gram.entry + val command : vernac_expr Gram.entry + val syntax : vernac_expr Gram.entry + val vernac : vernac_expr Gram.entry + val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry + val vernac_eoi : vernac_expr Gram.entry + val noedit_mode : vernac_expr Gram.entry + val command_entry : vernac_expr Gram.entry + val red_expr : raw_red_expr Gram.entry + val hint_info : Vernacexpr.hint_info_expr Gram.entry + end + + val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option + + val get_command_entry : unit -> vernac_expr Gram.entry + val set_command_entry : vernac_expr Gram.entry -> unit + + type gram_reinit = gram_assoc * gram_position + val grammar_extend : 'a Gram.entry -> gram_reinit option -> + 'a Extend.extend_statment -> unit + + module GramState : Store.S + + type 'a grammar_command + + type extend_rule = + | ExtendRule : 'a Gram.entry * gram_reinit option * 'a extend_statment -> extend_rule + + type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t + + val create_grammar_command : string -> 'a grammar_extension -> 'a grammar_command + + val extend_grammar_command : 'a grammar_command -> 'a -> unit + val recover_grammar_command : 'a grammar_command -> 'a list + val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b + + val to_coqloc : Ploc.t -> Loc.t + val (!@) : Ploc.t -> Loc.t + +end + +module Egramml : +sig + open Vernacexpr + + type 's grammar_prod_item = + | GramTerminal of string + | GramNonTerminal : ('a Genarg.raw_abstract_argument_type option * + ('s, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item + + val extend_vernac_command_grammar : + extend_name -> vernac_expr Pcoq.Gram.entry option -> + vernac_expr grammar_prod_item list -> unit + + val make_rule : + (Loc.t -> Genarg.raw_generic_argument list -> 'a) -> + 'a grammar_prod_item list -> 'a Extend.production_rule + +end (************************************************************************) (* End of modules from parsing/ *) @@ -4380,8 +5023,8 @@ end module Ind_tables : sig - type individual = Ind_tables.individual - type 'a scheme_kind = 'a Ind_tables.scheme_kind + type individual + type 'a scheme_kind val check_scheme : 'a scheme_kind -> Names.inductive -> bool val find_scheme : ?mode:Declare.internal_flag -> 'a scheme_kind -> Names.inductive -> Names.Constant.t * Safe_typing.private_constants @@ -4403,7 +5046,8 @@ sig type change_arg = Pattern.patvar_map -> Evd.evar_map -> Evd.evar_map * EConstr.constr type tactic_reduction = Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr - type elim_scheme = Tactics.elim_scheme = + + type elim_scheme = { elimc: EConstr.constr Misctypes.with_bindings option; elimt: EConstr.types; @@ -4611,7 +5255,8 @@ sig orientation -> Locus.occurrences -> freeze_evars_flag -> dep_proof_flag -> ?tac:(unit Proofview.tactic * conditions) -> EConstr.constr Misctypes.with_bindings -> Misctypes.evars_flag -> unit Proofview.tactic val subst : Names.Id.t list -> unit Proofview.tactic - type subst_tactic_flags = Equality.subst_tactic_flags = { + + type subst_tactic_flags = { only_leibniz : bool; rewrite_dependent_proof : bool } @@ -4671,21 +5316,36 @@ end module Hints : sig - type hint = Hints.hint - type debug = Hints.debug = - | Debug | Info | Off - type 'a hints_path_atom_gen = 'a Hints.hints_path_atom_gen = + + type raw_hint = EConstr.t * EConstr.types * Univ.universe_context_set + + type 'a hint_ast = + | Res_pf of 'a (* Hint Apply *) + | ERes_pf of 'a (* Hint EApply *) + | Give_exact of 'a + | Res_pf_THEN_trivial_fail of 'a (* Hint Immediate *) + | Unfold_nth of Names.evaluable_global_reference (* Hint Unfold *) + | Extern of Genarg.glob_generic_argument (* Hint Extern *) + + type hint + + type debug = + | Debug | Info | Off + + type 'a hints_path_atom_gen = | PathHints of 'a list | PathAny - type hint_term = Hints.hint_term = + + type hint_term = | IsGlobRef of Globnames.global_reference | IsConstr of EConstr.constr * Univ.ContextSet.t + type hint_db_name = string type hint_info = (Names.Id.t list * Pattern.constr_pattern) Vernacexpr.hint_info_gen type hnf = bool type hints_path_atom = Globnames.global_reference hints_path_atom_gen - type 'a hints_path_gen = 'a Hints.hints_path_gen = + type 'a hints_path_gen = | PathAtom of 'a hints_path_atom_gen | PathStar of 'a hints_path_gen | PathSeq of 'a hints_path_gen * 'a hints_path_gen @@ -4695,7 +5355,7 @@ sig type hints_path = Globnames.global_reference hints_path_gen - type hints_entry = Hints.hints_entry = + type hints_entry = | HintsResolveEntry of (hint_info * Decl_kinds.polymorphic * hnf * hints_path_atom * hint_term) list | HintsImmediateEntry of (hints_path_atom * Decl_kinds.polymorphic * hint_term) list | HintsCutEntry of hints_path @@ -4704,15 +5364,7 @@ sig | HintsModeEntry of Globnames.global_reference * Vernacexpr.hint_mode list | HintsExternEntry of hint_info * Genarg.glob_generic_argument - type 'a hint_ast = 'a Hints.hint_ast = - | Res_pf of 'a - | ERes_pf of 'a - | Give_exact of 'a - | Res_pf_THEN_trivial_fail of 'a - | Unfold_nth of Names.evaluable_global_reference - | Extern of Genarg.glob_generic_argument - type raw_hint = EConstr.constr * EConstr.types * Univ.ContextSet.t - type 'a with_metadata = 'a Hints.with_metadata = private { + type 'a with_metadata = private { pri : int; poly : Decl_kinds.polymorphic; pat : Pattern.constr_pattern option; @@ -4725,7 +5377,7 @@ sig module Hint_db : sig - type t = Hints.Hint_db.t + type t val empty : ?name:hint_db_name -> Names.transparent_state -> bool -> t val transparent_state : t -> Names.transparent_state val iter : (Globnames.global_reference option -> @@ -4784,9 +5436,11 @@ end module Class_tactics : sig - type search_strategy = Class_tactics.search_strategy = + + type search_strategy = | Dfs | Bfs + val set_typeclasses_debug : bool -> unit val set_typeclasses_strategy : search_strategy -> unit val set_typeclasses_depth : int option -> unit @@ -4841,7 +5495,9 @@ end module Lemmas : sig - type 'a declaration_hook = 'a Lemmas.declaration_hook + + type 'a declaration_hook + val mk_hook : (Decl_kinds.locality -> Globnames.global_reference -> 'a) -> 'a declaration_hook val start_proof : Names.Id.t -> ?pl:Proof_global.universe_binders -> Decl_kinds.goal_kind -> Evd.evar_map -> @@ -4876,9 +5532,19 @@ sig val make_module_locality : bool option -> bool end +module Metasyntax : +sig + + val add_token_obj : string -> unit + + type any_entry = AnyEntry : 'a Pcoq.Gram.entry -> any_entry + val register_grammar : string -> any_entry list -> unit + +end + module Search : sig - type glob_search_about_item = Search.glob_search_about_item = + type glob_search_about_item = | GlobSearchSubPattern of Pattern.constr_pattern | GlobSearchString of string type filter_function = Globnames.global_reference -> Environ.env -> Constr.t -> bool @@ -4904,10 +5570,32 @@ end module Command : sig - type structured_fixpoint_expr = Command.structured_fixpoint_expr + open Names + open Constrexpr + open Vernacexpr + + type structured_fixpoint_expr = { + fix_name : Id.t; + fix_univs : lident list option; + fix_annot : Id.t Loc.located option; + fix_binders : local_binder_expr list; + fix_body : constr_expr option; + fix_type : constr_expr + } + + type structured_one_inductive_expr = { + ind_name : Id.t; + ind_univs : lident list option; + ind_arity : constr_expr; + ind_lc : (Id.t * constr_expr) list + } + + type structured_inductive_expr = + local_binder_expr list * structured_one_inductive_expr list + type recursive_preentry = Names.Id.t list * Constr.t option list * Constr.types list - type structured_inductive_expr = Command.structured_inductive_expr - type one_inductive_impls = Command.one_inductive_impls + + type one_inductive_impls val do_mutual_inductive : (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic -> @@ -4963,6 +5651,17 @@ sig Names.Id.t end +module Vernacinterp : +sig + type deprecation = bool + + type vernac_command = Genarg.raw_generic_argument list -> unit -> unit + + val vinterp_add : deprecation -> Vernacexpr.extend_name -> + vernac_command -> unit + +end + module Mltop : sig val declare_cache_obj : (unit -> unit) -> string -> unit @@ -5004,6 +5703,38 @@ sig val classify_vernac : Vernacexpr.vernac_expr -> Vernacexpr.vernac_classification end +module Stm : +sig + type state + val state_of_id : + Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ] +end + (************************************************************************) (* End of modules from stm/ *) (************************************************************************) + +(************************************************************************) +(* Modules from highparsing/ *) +(************************************************************************) + +module G_vernac : +sig + + val def_body : Vernacexpr.definition_expr Pcoq.Gram.entry + val section_subset_expr : Vernacexpr.section_subset_expr Pcoq.Gram.entry + val query_command : (Vernacexpr.goal_selector option -> Vernacexpr.vernac_expr) Pcoq.Gram.entry + +end + +module G_proofs : +sig + + val hint : Vernacexpr.hints_expr Pcoq.Gram.entry + val hint_proof_using : 'a Pcoq.Gram.entry -> 'a option -> 'a option + +end + +(************************************************************************) +(* End of modules from highparsing/ *) +(************************************************************************) diff --git a/API/API.mllib b/API/API.mllib index f4bdf83db..25275c704 100644 --- a/API/API.mllib +++ b/API/API.mllib @@ -1,2 +1 @@ API -Grammar_API diff --git a/API/grammar_API.ml b/API/grammar_API.ml deleted file mode 100644 index 485c16665..000000000 --- a/API/grammar_API.ml +++ /dev/null @@ -1,63 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -module G_proofs = G_proofs -module Metasyntax = Metasyntax -module Egramcoq = Egramcoq -module G_vernac = G_vernac -module Pcoq = Pcoq -module Tok = Tok -module CLexer = CLexer -module Egramml = Egramml -module Mltop = Mltop -module Vernacinterp = Vernacinterp -module Genintern = Genintern - -module Extend = - struct - type 'a entry = 'a Extend.entry - type ('self, 'a) symbol = ('self, 'a) Extend.symbol = - | Atoken : Tok.t -> ('self, string) symbol - | Alist1 : ('self, 'a) symbol -> ('self, 'a list) symbol - | Alist1sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol - | Alist0 : ('self, 'a) symbol -> ('self, 'a list) symbol - | Alist0sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol - | Aopt : ('self, 'a) symbol -> ('self, 'a option) symbol - | Aself : ('self, 'self) symbol - | Anext : ('self, 'self) symbol - | Aentry : 'a entry -> ('self, 'a) symbol - | Aentryl : 'a entry * int -> ('self, 'a) symbol - | Arules : 'a rules list -> ('self, 'a) symbol - and ('self, 'a, 'r) rule = ('self, 'a, 'r) Extend.rule = - | Stop : ('self, 'r, 'r) rule - | Next : ('self, 'a, 'r) rule * ('self, 'b) symbol -> ('self, 'b -> 'a, 'r) rule - and ('a, 'r) norec_rule = ('a, 'r) Extend.norec_rule = - { norec_rule : 's. ('s, 'a, 'r) rule } - and 'a rules = 'a Extend.rules = - | Rules : ('act, Loc.t -> 'a) norec_rule * 'act -> 'a rules - type gram_assoc = Extend.gram_assoc = NonA | RightA | LeftA - type 'a production_rule = 'a Extend.production_rule = - | Rule : ('a, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule - type 'a single_extend_statment = string option * gram_assoc option * 'a production_rule list - type gram_position = Extend.gram_position = - | First - | Last - | Before of string - | After of string - | Level of string - type 'a extend_statment = Extend.gram_position option * 'a single_extend_statment list - - type 'a user_symbol = 'a Extend.user_symbol = - | Ulist1 of 'a user_symbol - | Ulist1sep of 'a user_symbol * string - | Ulist0 of 'a user_symbol - | Ulist0sep of 'a user_symbol * string - | Uopt of 'a user_symbol - | Uentry of 'a - | Uentryl of 'a * int - end diff --git a/API/grammar_API.mli b/API/grammar_API.mli deleted file mode 100644 index c2115a506..000000000 --- a/API/grammar_API.mli +++ /dev/null @@ -1,249 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -module Extend : -sig - type 'a entry = 'a Pcoq.Gram.Entry.e - type ('self, 'a) symbol = ('self, 'a) Extend.symbol = - | Atoken : Tok.t -> ('self, string) symbol - | Alist1 : ('self, 'a) symbol -> ('self, 'a list) symbol - | Alist1sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol - | Alist0 : ('self, 'a) symbol -> ('self, 'a list) symbol - | Alist0sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol - | Aopt : ('self, 'a) symbol -> ('self, 'a option) symbol - | Aself : ('self, 'self) symbol - | Anext : ('self, 'self) symbol - | Aentry : 'a entry -> ('self, 'a) symbol - | Aentryl : 'a entry * int -> ('self, 'a) symbol - | Arules : 'a rules list -> ('self, 'a) symbol - and ('self, 'a, 'r) rule = ('self, 'a, 'r) Extend.rule = - | Stop : ('self, 'r, 'r) rule - | Next : ('self, 'a, 'r) rule * ('self, 'b) symbol -> ('self, 'b -> 'a, 'r) rule - and ('a, 'r) norec_rule = ('a, 'r) Extend.norec_rule = - { norec_rule : 's. ('s, 'a, 'r) rule } - and 'a rules = 'a Extend.rules = - | Rules : ('act, Loc.t -> 'a) norec_rule * 'act -> 'a rules - type gram_assoc = Extend.gram_assoc = NonA | RightA | LeftA - type 'a production_rule = 'a Extend.production_rule = - | Rule : ('a, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule - type 'a single_extend_statment = string option * gram_assoc option * 'a production_rule list - type gram_position = Extend.gram_position = - | First - | Last - | Before of string - | After of string - | Level of string - type 'a extend_statment = gram_position option * 'a single_extend_statment list - type 'a user_symbol = 'a Extend.user_symbol = - | Ulist1 of 'a user_symbol - | Ulist1sep of 'a user_symbol * string - | Ulist0 of 'a user_symbol - | Ulist0sep of 'a user_symbol * string - | Uopt of 'a user_symbol - | Uentry of 'a - | Uentryl of 'a * int -end - -module Genintern : -sig - open API - module Store : module type of struct include Genintern.Store end - type glob_sign = Genintern.glob_sign = - { ltacvars : Names.Id.Set.t; - genv : Environ.env; - extra : Store.t } - type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb - type 'glb subst_fun = Mod_subst.substitution -> 'glb -> 'glb - type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Names.Id.Map.t -> 'glb -> 'glb - val empty_glob_sign : Environ.env -> glob_sign - val register_intern0 : ('raw, 'glb, 'top) Genarg.genarg_type -> - ('raw, 'glb) intern_fun -> unit - val register_subst0 : ('raw, 'glb, 'top) Genarg.genarg_type -> - 'glb subst_fun -> unit - val register_ntn_subst0 : ('raw, 'glb, 'top) Genarg.genarg_type -> - 'glb ntn_subst_fun -> unit - val generic_substitute : Genarg.glob_generic_argument subst_fun - val generic_intern : (Genarg.raw_generic_argument, Genarg.glob_generic_argument) intern_fun -end - -module Tok : -sig - type t = Tok.t = - | KEYWORD of string - | PATTERNIDENT of string - | IDENT of string - | FIELD of string - | INT of string - | STRING of string - | LEFTQMARK - | BULLET of string - | EOI -end - -module Pcoq : -sig - type gram_universe = Pcoq.gram_universe - module Gram : - sig - type te = Tok.t - module Entry : - sig - type 'a e = 'a Extend.entry - val of_parser : string -> (te Stream.t -> 'a) -> 'a e - val obj : 'a e -> te Gramext.g_entry - val create : string -> 'a e - end - type 'a entry = 'a Entry.e - val extend : 'a Pcoq.Gram.Entry.e -> Gramext.position option -> - (string option * Gramext.g_assoc option * - (Tok.t Gramext.g_symbol list * Gramext.g_action) list) list -> unit - val entry_create : string -> 'a Entry.e - end - module Prim : sig - open Names - open Loc - val preident : string Gram.Entry.e - val ident : Names.Id.t Gram.Entry.e - val name : Name.t located Gram.Entry.e - val identref : Names.Id.t located Gram.Entry.e - val pidentref : (Names.Id.t located * (Names.Id.t located list) option) Gram.Entry.e - val pattern_ident : Names.Id.t Gram.Entry.e - val pattern_identref : Names.Id.t located Gram.Entry.e - val base_ident : Names.Id.t Gram.Entry.e - val natural : int Gram.Entry.e - val bigint : Constrexpr.raw_natural_number Gram.Entry.e - val integer : int Gram.Entry.e - val string : string Gram.Entry.e - val qualid : API.Libnames.qualid located Gram.Entry.e - val fullyqualid : Names.Id.t list located Gram.Entry.e - val reference : API.Libnames.reference Gram.Entry.e - val by_notation : (string * string option) Loc.located Gram.entry - val smart_global : API.Libnames.reference API.Misctypes.or_by_notation Gram.Entry.e - val dirpath : DirPath.t Gram.Entry.e - val ne_string : string Gram.Entry.e - val ne_lstring : string located Gram.Entry.e - val var : Names.Id.t located Gram.Entry.e - end - - val eoi_entry : 'a Gram.Entry.e -> 'a Gram.Entry.e - val create_generic_entry : gram_universe -> string -> - ('a, Genarg.rlevel) Genarg.abstract_argument_type -> 'a Gram.Entry.e - val utactic : gram_universe - type gram_reinit = Extend.gram_assoc * Extend.gram_position - val grammar_extend : 'a Gram.Entry.e -> gram_reinit option -> - 'a Extend.extend_statment -> unit - val genarg_grammar : ('raw, 'glb, 'top) Genarg.genarg_type -> 'raw Gram.Entry.e - val register_grammar : ('raw, 'glb, 'top) Genarg.genarg_type -> 'raw Gram.Entry.e -> unit - module Constr : - sig - val sort : API.Misctypes.glob_sort Gram.Entry.e - val lconstr : API.Constrexpr.constr_expr Gram.Entry.e - val lconstr_pattern : API.Constrexpr.constr_expr Gram.Entry.e - val ident : API.Names.Id.t Gram.Entry.e - val constr : API.Constrexpr.constr_expr Gram.Entry.e - val closed_binder : API.Constrexpr.local_binder_expr list Gram.Entry.e - val constr_pattern : API.Constrexpr.constr_expr Gram.Entry.e - val global : API.Libnames.reference Gram.Entry.e - val binder_constr : API.Constrexpr.constr_expr Gram.Entry.e - val operconstr : API.Constrexpr.constr_expr Gram.Entry.e - val pattern : API.Constrexpr.cases_pattern_expr Gram.Entry.e - val binders : API.Constrexpr.local_binder_expr list Gram.Entry.e - end - module Vernac_ : - sig - val gallina : API.Vernacexpr.vernac_expr Gram.Entry.e - val gallina_ext : API.Vernacexpr.vernac_expr Gram.Entry.e - val red_expr : API.Genredexpr.raw_red_expr Gram.Entry.e - val noedit_mode : API.Vernacexpr.vernac_expr Gram.Entry.e - val command : API.Vernacexpr.vernac_expr Gram.Entry.e - val rec_definition : (API.Vernacexpr.fixpoint_expr * API.Vernacexpr.decl_notation list) Gram.Entry.e - val vernac : API.Vernacexpr.vernac_expr Gram.Entry.e - end - - type extend_rule = - | ExtendRule : 'a Gram.Entry.e * gram_reinit option * 'a Extend.extend_statment -> extend_rule - - module GramState : module type of struct include Pcoq.GramState end - type 'a grammar_command = 'a Pcoq.grammar_command - type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t - val create_grammar_command : string -> 'a grammar_extension -> 'a grammar_command - val extend_grammar_command : 'a grammar_command -> 'a -> unit - val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option - val parse_string : 'a Gram.Entry.e -> string -> 'a - val (!@) : Ploc.t -> Loc.t - val set_command_entry : API.Vernacexpr.vernac_expr Gram.Entry.e -> unit - val to_coqloc : Ploc.t -> Loc.t -end - -module CLexer : -sig - type keyword_state = CLexer.keyword_state - val terminal : string -> Tok.t - val add_keyword : string -> unit - val is_keyword : string -> bool - val check_ident : string -> unit - val get_keyword_state : unit -> keyword_state - val set_keyword_state : keyword_state -> unit -end - -module Egramml : -sig - type 's grammar_prod_item = 's Egramml.grammar_prod_item = - | GramTerminal of string - | GramNonTerminal : ('a Genarg.raw_abstract_argument_type option * - ('s, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item - - - val extend_vernac_command_grammar : - API.Vernacexpr.extend_name -> Vernacexpr.vernac_expr Pcoq.Gram.Entry.e option -> - Vernacexpr.vernac_expr grammar_prod_item list -> unit - - val make_rule : - (Loc.t -> Genarg.raw_generic_argument list -> 'a) -> - 'a grammar_prod_item list -> 'a Extend.production_rule -end - -module Mltop : -sig - val add_known_module : string -> unit - val module_is_known : string -> bool - val declare_cache_obj : (unit -> unit) -> string -> unit -end -module Vernacinterp : -sig - type deprecation = bool - type vernac_command = Genarg.raw_generic_argument list -> unit -> unit - val vinterp_add : deprecation -> API.Vernacexpr.extend_name -> - vernac_command -> unit -end - -module G_vernac : -sig - val def_body : API.Vernacexpr.definition_expr Pcoq.Gram.Entry.e - val section_subset_expr : API.Vernacexpr.section_subset_expr Pcoq.Gram.Entry.e - val query_command : (Vernacexpr.goal_selector option -> Vernacexpr.vernac_expr) - Pcoq.Gram.Entry.e -end - -module G_proofs : -sig - val hint : Vernacexpr.hints_expr Pcoq.Gram.Entry.e - val hint_proof_using : 'a Pcoq.Gram.Entry.e -> 'a option -> 'a option -end - -module Egramcoq : -sig -end - -module Metasyntax : -sig - type any_entry = Metasyntax.any_entry = - | AnyEntry : 'a Pcoq.Gram.Entry.e -> any_entry - val register_grammar : string -> any_entry list -> unit - val add_token_obj : string -> unit -end diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 9884a0109..ffa8fffdf 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -229,7 +229,7 @@ let ppenvwithcst e = pp str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++ str "{" ++ Cmap_env.fold (fun a _ s -> pr_con a ++ spc () ++ s) (Obj.magic e).Pre_env.env_globals.Pre_env.env_constants (mt ()) ++ str "}") -let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (Global.env()) x)) +let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (API.Global.env()) x)) let ppobj obj = Format.print_string (Libobject.object_tag obj) @@ -494,7 +494,6 @@ VERNAC COMMAND EXTEND PrintConstr END *) -open Grammar_API open Genarg open Stdarg open Egramml diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp index cc92680fc..643b6277a 100644 --- a/grammar/argextend.mlp +++ b/grammar/argextend.mlp @@ -46,17 +46,17 @@ let make_act loc act pil = make (List.rev pil) let make_prod_item = function - | ExtTerminal s -> <:expr< Grammar_API.Extend.Atoken (Grammar_API.CLexer.terminal $mlexpr_of_string s$) >> + | ExtTerminal s -> <:expr< Extend.Atoken (CLexer.terminal $mlexpr_of_string s$) >> | ExtNonTerminal (g, _) -> let base s = <:expr< $lid:s$ >> in mlexpr_of_prod_entry_key base g let rec make_prod = function -| [] -> <:expr< Grammar_API.Extend.Stop >> -| item :: prods -> <:expr< Grammar_API.Extend.Next $make_prod prods$ $make_prod_item item$ >> +| [] -> <:expr< Extend.Stop >> +| item :: prods -> <:expr< Extend.Next $make_prod prods$ $make_prod_item item$ >> let make_rule loc (prods,act) = - <:expr< Grammar_API.Extend.Rule $make_prod (List.rev prods)$ $make_act loc act prods$ >> + <:expr< Extend.Rule $make_prod (List.rev prods)$ $make_act loc act prods$ >> let is_ident x = function | <:expr< $lid:s$ >> -> (s : string) = x @@ -67,7 +67,7 @@ let make_extend loc s cl wit = match cl with (** Special handling of identity arguments by not redeclaring an entry *) <:str_item< value $lid:s$ = - let () = Grammar_API.Pcoq.register_grammar $wit$ $lid:e$ in + let () = Pcoq.register_grammar $wit$ $lid:e$ in $lid:e$ >> | _ -> @@ -75,8 +75,8 @@ let make_extend loc s cl wit = match cl with let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in <:str_item< value $lid:s$ = - let $lid:s$ = Grammar_API.Pcoq.create_generic_entry Grammar_API.Pcoq.utactic $se$ (Genarg.rawwit $wit$) in - let () = Grammar_API.Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]) in + let $lid:s$ = Pcoq.create_generic_entry Pcoq.utactic $se$ (Genarg.rawwit $wit$) in + let () = Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]) in $lid:s$ >> let warning_redundant prefix s = @@ -127,7 +127,7 @@ let declare_tactic_argument loc s (typ, f, g, h) cl = begin match globtyp with | None -> let typ = match globtyp with None -> ExtraArgType s | Some typ -> typ in - <:expr< fun ist v -> API.Ftactic.return (API.Geninterp.Val.inject (API.Geninterp.val_tag $make_topwit loc typ$) v) >> + <:expr< fun ist v -> Ftactic.return (Geninterp.Val.inject (Geninterp.val_tag $make_topwit loc typ$) v) >> | Some globtyp -> <:expr< fun ist x -> Tacinterp.interp_genarg ist (Genarg.in_gen $make_globwit loc globtyp$ x) >> @@ -137,10 +137,10 @@ let declare_tactic_argument loc s (typ, f, g, h) cl = let typ = match globtyp with None -> ExtraArgType s | Some typ -> typ in <:expr< let f = $lid:f$ in - fun ist v -> API.Ftactic.nf_enter (fun gl -> - let (sigma, v) = API.Tacmach.New.of_old (fun gl -> f ist gl v) gl in - let v = API.Geninterp.Val.inject (API.Geninterp.val_tag $make_topwit loc typ$) v in - API.Proofview.tclTHEN (API.Proofview.Unsafe.tclEVARS sigma) (API.Ftactic.return v) + fun ist v -> Ftactic.nf_enter (fun gl -> + let (sigma, v) = Tacmach.New.of_old (fun gl -> f ist gl v) gl in + let v = Geninterp.Val.inject (Geninterp.val_tag $make_topwit loc typ$) v in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Ftactic.return v) ) >> in let subst = match h with @@ -156,15 +156,15 @@ let declare_tactic_argument loc s (typ, f, g, h) cl = | Some f -> <:expr< $lid:f$>> in let dyn = match typ with | None -> <:expr< None >> - | Some typ -> <:expr< Some (API.Geninterp.val_tag $make_topwit loc typ$) >> + | Some typ -> <:expr< Some (Geninterp.val_tag $make_topwit loc typ$) >> in let wit = <:expr< $lid:"wit_"^s$ >> in declare_str_items loc [ <:str_item< value ($lid:"wit_"^s$) = Genarg.make0 $se$ >>; - <:str_item< Grammar_API.Genintern.register_intern0 $wit$ $glob$ >>; - <:str_item< Grammar_API.Genintern.register_subst0 $wit$ $subst$ >>; - <:str_item< API.Geninterp.register_interp0 $wit$ $interp$ >>; - <:str_item< API.Geninterp.register_val0 $wit$ $dyn$ >>; + <:str_item< Genintern.register_intern0 $wit$ $glob$ >>; + <:str_item< Genintern.register_subst0 $wit$ $subst$ >>; + <:str_item< Geninterp.register_interp0 $wit$ $interp$ >>; + <:str_item< Geninterp.register_val0 $wit$ $dyn$ >>; make_extend loc s cl wit; <:str_item< do { Pptactic.declare_extra_genarg_pprule diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp index 51a4c3573..536ee7ca5 100644 --- a/grammar/q_util.mlp +++ b/grammar/q_util.mlp @@ -57,23 +57,23 @@ let mlexpr_of_option f = function | Some e -> <:expr< Some $f e$ >> let mlexpr_of_name f = function - | None -> <:expr< API.Names.Name.Anonymous >> - | Some e -> <:expr< API.Names.Name.Name $f e$ >> + | None -> <:expr< Names.Name.Anonymous >> + | Some e -> <:expr< Names.Name.Name $f e$ >> -let symbol_of_string s = <:expr< Grammar_API.Extend.Atoken (Grammar_API.CLexer.terminal $str:s$) >> +let symbol_of_string s = <:expr< Extend.Atoken (CLexer.terminal $str:s$) >> let rec mlexpr_of_prod_entry_key f = function - | Ulist1 s -> <:expr< Grammar_API.Extend.Alist1 $mlexpr_of_prod_entry_key f s$ >> - | Ulist1sep (s,sep) -> <:expr< Grammar_API.Extend.Alist1sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >> - | Ulist0 s -> <:expr< Grammar_API.Extend.Alist0 $mlexpr_of_prod_entry_key f s$ >> - | Ulist0sep (s,sep) -> <:expr< Grammar_API.Extend.Alist0sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >> - | Uopt s -> <:expr< Grammar_API.Extend.Aopt $mlexpr_of_prod_entry_key f s$ >> - | Uentry e -> <:expr< Grammar_API.Extend.Aentry ($f e$) >> + | Ulist1 s -> <:expr< Extend.Alist1 $mlexpr_of_prod_entry_key f s$ >> + | Ulist1sep (s,sep) -> <:expr< Extend.Alist1sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >> + | Ulist0 s -> <:expr< Extend.Alist0 $mlexpr_of_prod_entry_key f s$ >> + | Ulist0sep (s,sep) -> <:expr< Extend.Alist0sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >> + | Uopt s -> <:expr< Extend.Aopt $mlexpr_of_prod_entry_key f s$ >> + | Uentry e -> <:expr< Extend.Aentry ($f e$) >> | Uentryl (e, l) -> (** Keep in sync with Pcoq! *) assert (e = "tactic"); - if l = 5 then <:expr< Grammar_API.Extend.Aentry Pltac.binder_tactic >> - else <:expr< Grammar_API.Extend.Aentryl (Pltac.tactic_expr) $mlexpr_of_int l$ >> + if l = 5 then <:expr< Extend.Aentry Pltac.binder_tactic >> + else <:expr< Extend.Aentryl (Pltac.tactic_expr) $mlexpr_of_int l$ >> let rec type_of_user_symbol = function | Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) -> diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index 079d2e4e4..0b33dab05 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -25,7 +25,7 @@ let plugin_name = <:expr< __coq_plugin_name >> let mlexpr_of_ident id = (** Workaround for badly-designed generic arguments lacking a closure *) let id = "$" ^ id in - <:expr< API.Names.Id.of_string_soft $str:id$ >> + <:expr< Names.Id.of_string_soft $str:id$ >> let rec make_patt = function | [] -> <:patt< [] >> @@ -57,18 +57,18 @@ let make_fun_clauses loc s l = let get_argt e = <:expr< (fun e -> match e with [ Genarg.ExtraArg tag -> tag | _ -> assert False ]) $e$ >> let rec mlexpr_of_symbol = function -| Ulist1 s -> <:expr< Grammar_API.Extend.Ulist1 $mlexpr_of_symbol s$ >> -| Ulist1sep (s,sep) -> <:expr< Grammar_API.Extend.Ulist1sep $mlexpr_of_symbol s$ $str:sep$ >> -| Ulist0 s -> <:expr< Grammar_API.Extend.Ulist0 $mlexpr_of_symbol s$ >> -| Ulist0sep (s,sep) -> <:expr< Grammar_API.Extend.Ulist0sep $mlexpr_of_symbol s$ $str:sep$ >> -| Uopt s -> <:expr< Grammar_API.Extend.Uopt $mlexpr_of_symbol s$ >> +| Ulist1 s -> <:expr< Extend.Ulist1 $mlexpr_of_symbol s$ >> +| Ulist1sep (s,sep) -> <:expr< Extend.Ulist1sep $mlexpr_of_symbol s$ $str:sep$ >> +| Ulist0 s -> <:expr< Extend.Ulist0 $mlexpr_of_symbol s$ >> +| Ulist0sep (s,sep) -> <:expr< Extend.Ulist0sep $mlexpr_of_symbol s$ $str:sep$ >> +| Uopt s -> <:expr< Extend.Uopt $mlexpr_of_symbol s$ >> | Uentry e -> let arg = get_argt <:expr< $lid:"wit_"^e$ >> in - <:expr< Grammar_API.Extend.Uentry (Genarg.ArgT.Any $arg$) >> + <:expr< Extend.Uentry (Genarg.ArgT.Any $arg$) >> | Uentryl (e, l) -> assert (e = "tactic"); let arg = get_argt <:expr< Tacarg.wit_tactic >> in - <:expr< Grammar_API.Extend.Uentryl (Genarg.ArgT.Any $arg$) $mlexpr_of_int l$>> + <:expr< Extend.Uentryl (Genarg.ArgT.Any $arg$) $mlexpr_of_int l$>> let make_prod_item = function | ExtTerminal s -> <:expr< Tacentries.TacTerm $str:s$ >> @@ -113,12 +113,12 @@ let declare_tactic loc tacname ~level classification clause = match clause with the ML tactic retrieves its arguments in the [ist] environment instead. This is the rôle of the [lift_constr_tac_to_ml_tac] function. *) let body = <:expr< Tacexpr.TacFun ($vars$, Tacexpr.TacML (Loc.tag ( $ml$ , []))) >> in - let name = <:expr< API.Names.Id.of_string $name$ >> in + let name = <:expr< Names.Id.of_string $name$ >> in declare_str_items loc [ <:str_item< do { let obj () = Tacenv.register_ltac True False $name$ $body$ in let () = Tacenv.register_ml_tactic $se$ [|$tac$|] in - API.Mltop.declare_cache_obj obj $plugin_name$ } >> + Mltop.declare_cache_obj obj $plugin_name$ } >> ] | _ -> (** Otherwise we add parsing and printing rules to generate a call to a @@ -131,7 +131,7 @@ let declare_tactic loc tacname ~level classification clause = match clause with declare_str_items loc [ <:str_item< do { Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc tacname clause$); - Grammar_API.Mltop.declare_cache_obj $obj$ $plugin_name$; } >> + Mltop.declare_cache_obj $obj$ $plugin_name$; } >> ] open Pcaml diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index af4d0dfe8..a529185dd 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -100,12 +100,12 @@ let make_fun_classifiers loc s c l = mlexpr_of_list (fun x -> x) cl let make_prod_item = function - | ExtTerminal s -> <:expr< Grammar_API.Egramml.GramTerminal $str:s$ >> + | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >> | ExtNonTerminal (g, ido) -> let nt = type_of_user_symbol g in - let base s = <:expr< Grammar_API.Pcoq.genarg_grammar ($mk_extraarg loc s$) >> in + let base s = <:expr< Pcoq.genarg_grammar ($mk_extraarg loc s$) >> in let typ = match ido with None -> None | Some _ -> Some nt in - <:expr< Grammar_API.Egramml.GramNonTerminal ( Loc.tag ( $mlexpr_of_option (make_rawwit loc) typ$ , + <:expr< Egramml.GramNonTerminal ( Loc.tag ( $mlexpr_of_option (make_rawwit loc) typ$ , $mlexpr_of_prod_entry_key base g$ ) ) >> let mlexpr_of_clause cl = @@ -122,9 +122,9 @@ let declare_command loc s c nt cl = let classl = make_fun_classifiers loc s c cl in declare_str_items loc [ <:str_item< do { - CList.iteri (fun i (depr, f) -> Grammar_API.Vernacinterp.vinterp_add depr ($se$, i) f) $funcl$; - CList.iteri (fun i f -> API.Vernac_classifier.declare_vernac_classifier ($se$, i) f) $classl$; - CList.iteri (fun i r -> Grammar_API.Egramml.extend_vernac_command_grammar ($se$, i) $nt$ r) $gl$; + CList.iteri (fun i (depr, f) -> Vernacinterp.vinterp_add depr ($se$, i) f) $funcl$; + CList.iteri (fun i f -> Vernac_classifier.declare_vernac_classifier ($se$, i) f) $classl$; + CList.iteri (fun i r -> Egramml.extend_vernac_command_grammar ($se$, i) $nt$ r) $gl$; } >> ] open Pcaml @@ -143,16 +143,16 @@ EXTEND | "DECLARE"; "PLUGIN"; name = STRING -> declare_str_items loc [ <:str_item< value __coq_plugin_name = $str:name$ >>; - <:str_item< value _ = Grammar_API.Mltop.add_known_module __coq_plugin_name >>; + <:str_item< value _ = Mltop.add_known_module __coq_plugin_name >>; ] ] ] ; classification: [ [ "CLASSIFIED"; "BY"; c = LIDENT -> <:expr< $lid:c$ >> | "CLASSIFIED"; "AS"; "SIDEFF" -> - <:expr< fun _ -> API.Vernac_classifier.classify_as_sideeff >> + <:expr< fun _ -> Vernac_classifier.classify_as_sideeff >> | "CLASSIFIED"; "AS"; "QUERY" -> - <:expr< fun _ -> API.Vernac_classifier.classify_as_query >> + <:expr< fun _ -> Vernac_classifier.classify_as_query >> ] ] ; deprecation: diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index dd3f9a2f8..994634854 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -9,15 +9,15 @@ Constr Context Vars Term -Declarations -Entries Mod_subst Cbytecodes Copcodes Cemitcodes +Opaqueproof +Declarations +Entries Nativevalues Primitives -Opaqueproof Declareops Retroknowledge Conv_oracle diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 4372ea557..2ce1b2be1 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Grammar_API.Pcoq.Prim +open Pcoq.Prim DECLARE PLUGIN "extraction_plugin" diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index c001ee382..1e7da3250 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Grammar_API open Ltac_plugin open Formula open Sequent diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index c495703ee..16d9f200f 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) (*i camlp4deps: "grammar/grammar.cma" i*) -open Grammar_API open Ltac_plugin open Util open Pp diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index 72c6f9090..609795133 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Grammar_API open Pp open Genarg open Stdarg diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index 419c5e8c4..acdf67779 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Grammar_API open Tacexpr open Names open Constrexpr diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 6d80ab549..f3f2f27e9 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Grammar_API open Pp open Genarg open Stdarg diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 4d13d89a4..301943a50 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Grammar_API open Pp open Genarg open Stdarg diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index cc052c8a2..2ea0f60eb 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -8,8 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Grammar_API - DECLARE PLUGIN "ltac_plugin" open Util diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index 1935d560a..1a2d89586 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -12,7 +12,6 @@ Syntax for the subtac terms and types. Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filli�tre *) -open Grammar_API open Libnames open Constrexpr open Constrexpr_ops diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index 3c27b2747..c874f8d5a 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -10,7 +10,6 @@ (* Syntax for rewriting with strategies *) -open Grammar_API open Names open Misctypes open Locus diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index e539b5867..d792d4ff7 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Grammar_API open Pp open CErrors open Util diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml index 2adcf02e6..2c1b1067e 100644 --- a/plugins/ltac/pltac.ml +++ b/plugins/ltac/pltac.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Grammar_API open Pcoq (* Main entry for extensions *) diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index 794cb527f..048dcc8e9 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -8,7 +8,6 @@ (** Ltac parsing entries *) -open Grammar_API open Loc open Names open Pcoq diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 791b7f48d..cf676f598 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Grammar_API open Pp open CErrors open Util diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index ccd44b914..aa8f4efe6 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -8,7 +8,6 @@ (** Ltac toplevel command entries. *) -open Grammar_API open Vernacexpr open Tacexpr diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index df03c7b47..0554d4364 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Grammar_API open Pattern open Pp open Genredexpr diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index ad2e70908..b262473a9 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Grammar_API open Pp open Names open Tacexpr diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 7b054947b..60a8f75ec 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Grammar_API open Constrintern open Patternops open Pp diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index c1ca85433..180fb2db4 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Grammar_API open Util open Tacexpr open Mod_subst diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index 6c82346bc..05ab8ab32 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Grammar_API open Ltac_plugin open Pp open Util diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 608b778e4..799e969ae 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open Grammar_API open Util open Names open Evd diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 228444b82..ce23bb2b3 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open Grammar_API open Names open Pp open Pcoq diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index c93e10405..bf6f44f11 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -8,8 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open Grammar_API - val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type val pr_ssrtacarg : 'a -> 'b -> (int * Ppextend.parenRelation -> 'c) -> 'c diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index fbe3cd2b9..9c59d83d4 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open Grammar_API open Names open Term open Termops diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 74519f6c5..f6300ab7e 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -8,8 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open Grammar_API - (* Defining grammar rules with "xx" in it automatically declares keywords too, * we thus save the lexer to restore it at the end of the file *) let frozen_lexer = CLexer.get_keyword_state () ;; diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 0c09d7bfb..65ea76d16 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -1,7 +1,6 @@ (* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) -open Grammar_API open Goal open Genarg open Tacexpr |