diff options
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.ml | 1 | ||||
| -rw-r--r-- | API/API.mli | 77 |
2 files changed, 51 insertions, 27 deletions
diff --git a/API/API.ml b/API/API.ml index 68da858ba0..46ad36d36d 100644 --- a/API/API.ml +++ b/API/API.ml @@ -162,6 +162,7 @@ module Indrec = Indrec (* module Cases *) module Pretyping = Pretyping module Unification = Unification +module Univdecls = Univdecls (******************************************************************************) (* interp *) (******************************************************************************) diff --git a/API/API.mli b/API/API.mli index 50fbee5298..3ed326ff0e 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1648,6 +1648,14 @@ sig type sort_info = Names.Name.t Loc.located list type glob_sort = sort_info glob_sort_gen + type ('a, 'b) gen_universe_decl = { + univdecl_instance : 'a; (* Declared universes *) + univdecl_extensible_instance : bool; (* Can new universes be added *) + univdecl_constraints : 'b; (* Declared constraints *) + univdecl_extensible_constraints : bool (* Can new constraints be added *) } + + type glob_constraint = glob_level * Univ.constraint_type * glob_level + type case_style = Term.case_style = | LetStyle | IfStyle @@ -2300,7 +2308,7 @@ sig val universe_context_set : evar_map -> Univ.ContextSet.t val evar_ident : evar -> evar_map -> Names.Id.t option val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list - val universe_context : ?names:(Names.Id.t Loc.located) list -> evar_map -> + val universe_context : names:(Names.Id.t Loc.located) list -> extensible:bool -> evar_map -> (Names.Id.t * Univ.Level.t) list * Univ.UContext.t val nf_constraints : evar_map -> evar_map val from_ctx : UState.t -> evar_map @@ -2461,7 +2469,6 @@ sig constr_expr list list * local_binder_expr list list - type typeclass_constraint = (Names.Name.t Loc.located * Names.Id.t Loc.located list option) * Decl_kinds.binding_kind * constr_expr type constr_pattern_expr = constr_expr end @@ -2744,15 +2751,15 @@ sig the whole identifier except for the {i subscript}. E.g. if we take [foo42], then [42] is the {i subscript}, and [foo] is the root. *) - val next_ident_away : Names.Id.t -> Names.Id.t list -> Names.Id.t + val next_ident_away : Names.Id.t -> Names.Id.Set.t -> Names.Id.t val hdchar : Environ.env -> Evd.evar_map -> EConstr.types -> string val id_of_name_using_hdchar : Environ.env -> Evd.evar_map -> EConstr.types -> Names.Name.t -> Names.Id.t - val next_ident_away_in_goal : Names.Id.t -> Names.Id.t list -> Names.Id.t + val next_ident_away_in_goal : Names.Id.t -> Names.Id.Set.t -> Names.Id.t val default_dependent_ident : Names.Id.t - val next_global_ident_away : Names.Id.t -> Names.Id.t list -> Names.Id.t + val next_global_ident_away : Names.Id.t -> Names.Id.Set.t -> Names.Id.t val rename_bound_vars_as_displayed : - Evd.evar_map -> Names.Id.t list -> Names.Name.t list -> EConstr.types -> EConstr.types + Evd.evar_map -> Names.Id.Set.t -> Names.Name.t list -> EConstr.types -> EConstr.types end module Termops : @@ -3663,7 +3670,7 @@ sig type lname = Names.Name.t Loc.located type lident = Names.Id.t Loc.located type opacity_flag = - | Opaque of lident list option + | Opaque | Transparent type locality_flag = bool type inductive_kind = @@ -3704,6 +3711,10 @@ sig type obsolete_locality = bool + type universe_decl_expr = (lident list, Misctypes.glob_constraint list) gen_universe_decl + + type ident_decl = lident * universe_decl_expr option + type lstring type 'a with_coercion = coercion_flag * 'a type scope_name = string @@ -3721,9 +3732,7 @@ sig | 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 inductive_expr = ident_decl with_coercion * Constrexpr.local_binder_expr list * Constrexpr.constr_expr option * inductive_kind * constructor_list_or_record_decl_expr type syntax_modifier = | SetItemLevel of string list * Extend.production_level @@ -3737,18 +3746,20 @@ sig type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation + type typeclass_constraint = (Names.Name.t Loc.located * universe_decl_expr option) * Decl_kinds.binding_kind * constr_expr + 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) + ident_decl 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 fixpoint_expr = ident_decl * (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 @@ -3826,12 +3837,12 @@ sig scope_name option | VernacNotationAddFormat of string * string * string | VernacDefinition of - (Decl_kinds.locality option * Decl_kinds.definition_object_kind) * plident * definition_expr + (Decl_kinds.locality option * Decl_kinds.definition_object_kind) * ident_decl * definition_expr | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list | VernacEndProof of proof_end | VernacExactProof of Constrexpr.constr_expr | VernacAssumption of (Decl_kinds.locality option * Decl_kinds.assumption_object_kind) * - inline * (plident list * Constrexpr.constr_expr) with_coercion list + inline * (ident_decl list * Constrexpr.constr_expr) with_coercion list | VernacInductive of cumulative_inductive_parsing_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of Decl_kinds.locality option * (fixpoint_expr * decl_notation list) list @@ -3855,7 +3866,7 @@ sig | VernacInstance of bool * Constrexpr.local_binder_expr list * - Constrexpr.typeclass_constraint * + typeclass_constraint * (bool * Constrexpr.constr_expr) option * hint_info_expr | VernacContext of Constrexpr.local_binder_expr list @@ -3946,7 +3957,7 @@ sig | SelectAll and vernac_classification = vernac_type * vernac_when and one_inductive_expr = - plident * Constrexpr.local_binder_expr list * Constrexpr.constr_expr option * constructor_expr list + ident_decl * Constrexpr.local_binder_expr list * Constrexpr.constr_expr option * constructor_expr list end (* XXX: end manual intf move *) @@ -4000,7 +4011,7 @@ sig | Later : [ `thunk ] delay val print_universes : bool ref val print_evar_arguments : bool ref - val detype : 'a delay -> ?lax:bool -> bool -> Names.Id.t list -> Environ.env -> Evd.evar_map -> EConstr.constr -> 'a Glob_term.glob_constr_g + val detype : 'a delay -> ?lax:bool -> bool -> Names.Id.Set.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> 'a Glob_term.glob_constr_g val subst_glob_constr : Mod_subst.substitution -> Glob_term.glob_constr -> Glob_term.glob_constr val set_detype_anonymous : (?loc:Loc.t -> int -> Names.Id.t) -> unit end @@ -4083,6 +4094,18 @@ sig Environ.env -> Evd.evar_map -> ?flags:unify_flags -> EConstr.constr * EConstr.constr -> Evd.evar_map * EConstr.constr end +module Univdecls : +sig + type universe_decl = + (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl + + val interp_univ_decl : Environ.env -> Vernacexpr.universe_decl_expr -> + Evd.evar_map * universe_decl + val interp_univ_decl_opt : Environ.env -> Vernacexpr.universe_decl_expr option -> + Evd.evar_map * universe_decl + val default_univ_decl : universe_decl +end + (************************************************************************) (* End of modules from pretyping/ *) (************************************************************************) @@ -4481,12 +4504,11 @@ sig 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 -> + Names.Id.t -> ?pl:Univdecls.universe_decl -> Decl_kinds.goal_kind -> Proofview.telescope -> proof_terminator -> unit val with_current_proof : (unit Proofview.tactic -> Proof.proof -> Proof.proof * 'a) -> 'a @@ -4606,6 +4628,7 @@ sig val pf_env : 'a Proofview.Goal.t -> Environ.env val pf_ids_of_hyps : 'a Proofview.Goal.t -> Names.Id.t list + val pf_ids_set_of_hyps : 'a Proofview.Goal.t -> Names.Id.Set.t val pf_concl : 'a Proofview.Goal.t -> EConstr.types val pf_get_new_id : Names.Id.t -> 'a Proofview.Goal.t -> Names.Id.t val pf_get_hyp_typ : Names.Id.t -> 'a Proofview.Goal.t -> EConstr.types @@ -5118,7 +5141,7 @@ sig val convert_concl : ?check:bool -> EConstr.types -> Constr.cast_kind -> unit tactic val intro_using : Names.Id.t -> unit tactic val intro : unit tactic - val fresh_id_in_env : Names.Id.t list -> Names.Id.t -> Environ.env -> Names.Id.t + val fresh_id_in_env : Names.Id.Set.t -> Names.Id.t -> Environ.env -> Names.Id.t val is_quantified_hypothesis : Names.Id.t -> 'a Goal.t -> bool val tclABSTRACT : ?opaque:bool -> Names.Id.t option -> unit Proofview.tactic -> unit Proofview.tactic val intro_patterns : bool -> Tactypes.intro_patterns -> unit Proofview.tactic @@ -5218,7 +5241,7 @@ sig val eapply_with_bindings : EConstr.constr Misctypes.with_bindings -> unit Proofview.tactic val assert_by : Names.Name.t -> EConstr.types -> unit Proofview.tactic -> unit Proofview.tactic - val intro_avoiding : Names.Id.t list -> unit Proofview.tactic + val intro_avoiding : Names.Id.Set.t -> unit Proofview.tactic val pose_proof : Names.Name.t -> EConstr.constr -> unit Proofview.tactic val pattern_option : (Locus.occurrences * EConstr.constr) list -> Locus.goal_location -> unit Proofview.tactic val compute_elim_sig : Evd.evar_map -> ?elimc:EConstr.constr Misctypes.with_bindings -> EConstr.types -> elim_scheme @@ -5540,7 +5563,7 @@ sig 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 -> + val start_proof : Names.Id.t -> ?pl:Univdecls.universe_decl -> Decl_kinds.goal_kind -> Evd.evar_map -> ?terminator:(Proof_global.lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) -> ?sign:Environ.named_context_val -> EConstr.types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> @@ -5616,7 +5639,7 @@ sig type structured_fixpoint_expr = { fix_name : Id.t; - fix_univs : lident list option; + fix_univs : universe_decl_expr option; fix_annot : Id.t Loc.located option; fix_binders : local_binder_expr list; fix_body : constr_expr option; @@ -5625,7 +5648,7 @@ sig type structured_one_inductive_expr = { ind_name : Id.t; - ind_univs : lident list option; + ind_univs : universe_decl_expr option; ind_arity : constr_expr; ind_lc : (Id.t * constr_expr) list } @@ -5641,7 +5664,7 @@ sig (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic -> Decl_kinds.private_flag -> Decl_kinds.recursivity_kind -> unit - val do_definition : Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.lident list option -> + 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 @@ -5654,7 +5677,7 @@ sig val interp_fixpoint : structured_fixpoint_expr list -> Vernacexpr.decl_notation list -> - recursive_preentry * Vernacexpr.lident list option * UState.t * + recursive_preentry * Univdecls.universe_decl * UState.t * (EConstr.rel_context * Impargs.manual_implicits * int option) list val extract_mutual_inductive_declaration_components : @@ -5682,7 +5705,7 @@ sig ?refine:bool -> Decl_kinds.polymorphic -> Constrexpr.local_binder_expr list -> - Constrexpr.typeclass_constraint -> + Vernacexpr.typeclass_constraint -> (bool * Constrexpr.constr_expr) option -> ?generalize:bool -> ?tac:unit Proofview.tactic -> |