diff options
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.ml | 4 | ||||
| -rw-r--r-- | API/API.mli | 74 |
2 files changed, 50 insertions, 28 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..a69766901b 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4620,6 +4620,9 @@ end module Constrintern : sig + + open Evd + type ltac_sign = { ltac_vars : Names.Id.Set.t; ltac_bound : Names.Id.Set.t; @@ -4635,11 +4638,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 +4660,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 @@ -6045,21 +6050,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 +6107,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 +6136,7 @@ sig ?abstract:bool -> ?global:bool -> ?refine:bool -> + program_mode:bool -> Decl_kinds.polymorphic -> Constrexpr.local_binder_expr list -> Vernacexpr.typeclass_constraint -> |