diff options
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.ml | 4 | ||||
| -rw-r--r-- | API/API.mli | 94 |
2 files changed, 62 insertions, 36 deletions
diff --git a/API/API.ml b/API/API.ml index 378c03ee4f..081ac2bb28 100644 --- a/API/API.ml +++ b/API/API.ml @@ -267,7 +267,9 @@ module Metasyntax = Metasyntax module Search = Search (* module Indschemes *) module Obligations = Obligations -module Command = Command +module ComDefinition = ComDefinition +module ComInductive = ComInductive +module ComFixpoint = ComFixpoint module Classes = Classes (* module Record *) (* module Assumptions *) diff --git a/API/API.mli b/API/API.mli index 8f46a58321..24a99d57f6 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4159,10 +4159,6 @@ sig type vernac_expr = | VernacLoad of verbose_flag * string - | VernacTime of vernac_expr Loc.located - | VernacRedirect of string * vernac_expr Loc.located - | VernacTimeout of int * vernac_expr - | VernacFail of vernac_expr | VernacSyntaxExtension of bool * (lstring * syntax_modifier list) | VernacOpenCloseScope of bool * scope_name | VernacDelimiters of scope_name * string option @@ -4294,6 +4290,16 @@ sig and vernac_classification = vernac_type * vernac_when and one_inductive_expr = ident_decl * Constrexpr.local_binder_expr list * Constrexpr.constr_expr option * constructor_expr list + +type vernac_control = + | VernacExpr of vernac_expr + (* Control *) + | VernacTime of vernac_control Loc.located + | VernacRedirect of string * vernac_control Loc.located + | VernacTimeout of int * vernac_control + | VernacFail of vernac_control + + end (* XXX: end of moved from intf *) @@ -4620,6 +4626,9 @@ end module Constrintern : sig + + open Evd + type ltac_sign = { ltac_vars : Names.Id.Set.t; ltac_bound : Names.Id.Set.t; @@ -4635,11 +4644,11 @@ sig | Variable type internalization_env = var_internalization_data Names.Id.Map.t - val interp_constr_evars : Environ.env -> Evd.evar_map ref -> - ?impls:internalization_env -> Constrexpr.constr_expr -> EConstr.constr + val interp_constr_evars : Environ.env -> evar_map -> + ?impls:internalization_env -> Constrexpr.constr_expr -> evar_map * EConstr.constr - val interp_type_evars : Environ.env -> Evd.evar_map ref -> - ?impls:internalization_env -> Constrexpr.constr_expr -> EConstr.types + val interp_type_evars : Environ.env -> Evd.evar_map -> + ?impls:internalization_env -> Constrexpr.constr_expr -> evar_map * EConstr.types val empty_ltac_sign : ltac_sign val intern_gen : Pretyping.typing_constraint -> Environ.env -> @@ -4657,10 +4666,12 @@ sig val locate_reference : Libnames.qualid -> Globnames.global_reference val interp_type : Environ.env -> Evd.evar_map -> ?impls:internalization_env -> Constrexpr.constr_expr -> Constr.types Evd.in_evar_universe_context + val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int -> - Environ.env -> Evd.evar_map ref -> Constrexpr.local_binder_expr list -> - internalization_env * ((Environ.env * EConstr.rel_context) * Impargs.manual_implicits) + Environ.env -> Evd.evar_map -> Constrexpr.local_binder_expr list -> + evar_map * (internalization_env * ((Environ.env * EConstr.rel_context) * Impargs.manual_implicits)) + val compute_internalization_data : Environ.env -> var_internalization_type -> Constr.types -> Impargs.manual_explicitation list -> var_internalization_data val empty_internalization_env : internalization_env @@ -5170,9 +5181,7 @@ sig 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 @@ -5968,7 +5977,7 @@ end module Ppvernac : sig - val pr_vernac : Vernacexpr.vernac_expr -> Pp.t + val pr_vernac : Vernacexpr.vernac_control -> Pp.t val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t end @@ -6045,21 +6054,53 @@ sig val show_term : Names.Id.t option -> Pp.t end -module Command : +module ComDefinition : sig + val do_definition : + program_mode:bool -> + Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.universe_decl_expr option -> + Constrexpr.local_binder_expr list -> Redexpr.red_expr option -> Constrexpr.constr_expr -> + Constrexpr.constr_expr option -> unit Lemmas.declaration_hook -> unit +end + +module ComFixpoint : +sig + open Names open Constrexpr - open Vernacexpr type structured_fixpoint_expr = { fix_name : Id.t; - fix_univs : universe_decl_expr option; + fix_univs : Vernacexpr.universe_decl_expr option; fix_annot : Id.t Loc.located option; fix_binders : local_binder_expr list; fix_body : constr_expr option; fix_type : constr_expr } + type recursive_preentry = Names.Id.t list * Constr.t option list * Constr.types list + + val interp_fixpoint : + cofix:bool -> + structured_fixpoint_expr list -> Vernacexpr.decl_notation list -> + recursive_preentry * Univdecls.universe_decl * UState.t * + (EConstr.rel_context * Impargs.manual_implicits * int option) list + + val extract_fixpoint_components : bool -> + (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> + structured_fixpoint_expr list * Vernacexpr.decl_notation list + + val do_fixpoint : + Decl_kinds.locality -> Decl_kinds.polymorphic -> (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> unit + +end + +module ComInductive : +sig + open Names + open Constrexpr + open Vernacexpr + type structured_one_inductive_expr = { ind_name : Id.t; ind_univs : universe_decl_expr option; @@ -6070,30 +6111,12 @@ sig 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 one_inductive_impls val do_mutual_inductive : (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic -> Decl_kinds.private_flag -> Declarations.recursivity_kind -> unit - val do_definition : Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.universe_decl_expr option -> - Constrexpr.local_binder_expr list -> Redexpr.red_expr option -> Constrexpr.constr_expr -> - Constrexpr.constr_expr option -> unit Lemmas.declaration_hook -> unit - - val do_fixpoint : - Decl_kinds.locality -> Decl_kinds.polymorphic -> (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> unit - - val extract_fixpoint_components : bool -> - (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> - structured_fixpoint_expr list * Vernacexpr.decl_notation list - - val interp_fixpoint : - structured_fixpoint_expr list -> Vernacexpr.decl_notation list -> - recursive_preentry * Univdecls.universe_decl * UState.t * - (EConstr.rel_context * Impargs.manual_implicits * int option) list - val extract_mutual_inductive_declaration_components : (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list -> structured_inductive_expr * Libnames.qualid list * Vernacexpr.decl_notation list @@ -6117,6 +6140,7 @@ sig ?abstract:bool -> ?global:bool -> ?refine:bool -> + program_mode:bool -> Decl_kinds.polymorphic -> Constrexpr.local_binder_expr list -> Vernacexpr.typeclass_constraint -> @@ -6201,7 +6225,7 @@ sig val classify_as_proofstep : Vernacexpr.vernac_classification val classify_as_query : Vernacexpr.vernac_classification val classify_as_sideeff : Vernacexpr.vernac_classification - val classify_vernac : Vernacexpr.vernac_expr -> Vernacexpr.vernac_classification + val classify_vernac : Vernacexpr.vernac_control -> Vernacexpr.vernac_classification end module Stm : |