diff options
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.ml | 3 | ||||
| -rw-r--r-- | API/API.mli | 30 |
2 files changed, 16 insertions, 17 deletions
diff --git a/API/API.ml b/API/API.ml index c952e123d..c4bcef6f6 100644 --- a/API/API.ml +++ b/API/API.ml @@ -43,7 +43,7 @@ module Cbytecodes = Cbytecodes (* module Copcodes *) module Cemitcodes = Cemitcodes (* module Nativevalues *) -(* module Primitives *) +(* module CPrimitives *) module Opaqueproof = Opaqueproof module Declareops = Declareops module Retroknowledge = Retroknowledge @@ -169,7 +169,6 @@ module Stdarg = Stdarg module Genintern = Genintern module Constrexpr_ops = Constrexpr_ops module Notation_ops = Notation_ops -module Ppextend = Ppextend module Notation = Notation module Dumpglob = Dumpglob (* module Syntax_def *) diff --git a/API/API.mli b/API/API.mli index f4a7be2a3..a90f8f84c 100644 --- a/API/API.mli +++ b/API/API.mli @@ -3184,6 +3184,10 @@ sig | NCast of notation_constr * notation_constr Misctypes.cast_type type interpretation = (Names.Id.t * (subscopes * notation_var_instance_type)) list * notation_constr + type precedence = int + type parenRelation = + | L | E | Any | Prec of precedence + type tolerability = precedence * parenRelation end module Tactypes : @@ -3782,6 +3786,12 @@ sig | DefaultInline | InlineAt of int + type cumulative_inductive_parsing_flag = + | GlobalCumulativity + | GlobalNonCumulativity + | LocalCumulativity + | LocalNonCumulativity + type vernac_expr = | VernacLoad of verbose_flag * string | VernacTime of vernac_expr Loc.located @@ -3806,7 +3816,7 @@ sig | 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 - | VernacInductive of Decl_kinds.cumulative_inductive_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) 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 | VernacCoFixpoint of @@ -4166,16 +4176,6 @@ sig 'a -> Notation_term.notation_constr -> Glob_term.glob_constr end -module Ppextend : -sig - - type precedence = int - type parenRelation = - | L | E | Any | Prec of precedence - type tolerability = precedence * parenRelation - -end - module Notation : sig type cases_pattern_status = bool @@ -4276,10 +4276,10 @@ module Constrextern : sig val extern_glob_constr : Names.Id.Set.t -> Glob_term.glob_constr -> Constrexpr.constr_expr val extern_glob_type : Names.Id.Set.t -> Glob_term.glob_constr -> Constrexpr.constr_expr - val extern_constr : ?lax:bool -> bool -> Environ.env -> Evd.evar_map -> Constr.t -> Constrexpr.constr_expr + val extern_constr : ?lax:bool -> bool -> Environ.env -> Evd.evar_map -> EConstr.t -> Constrexpr.constr_expr val without_symbols : ('a -> 'b) -> 'a -> 'b val print_universes : bool ref - val extern_type : bool -> Environ.env -> Evd.evar_map -> Term.types -> Constrexpr.constr_expr + val extern_type : bool -> Environ.env -> Evd.evar_map -> EConstr.t -> Constrexpr.constr_expr val with_universes : ('a -> 'b) -> 'a -> 'b val set_extern_reference : (?loc:Loc.t -> Names.Id.Set.t -> Globnames.global_reference -> Libnames.reference) -> unit @@ -4869,7 +4869,7 @@ sig val pr_with_comments : ?loc:Loc.t -> Pp.t -> Pp.t val pr_lident : Names.Id.t Loc.located -> Pp.t val pr_lname : Names.Name.t Loc.located -> Pp.t - val prec_less : int -> int * Ppextend.parenRelation -> bool + val prec_less : int -> int * Notation_term.parenRelation -> bool val pr_constr_expr : Constrexpr.constr_expr -> Pp.t val pr_lconstr_expr : Constrexpr.constr_expr -> Pp.t val pr_constr_pattern_expr : Constrexpr.constr_pattern_expr -> Pp.t @@ -5230,7 +5230,7 @@ sig val build_selector : Environ.env -> Evd.evar_map -> int -> EConstr.constr -> EConstr.types -> - EConstr.constr -> EConstr.constr -> Evd.evar_map * EConstr.constr + EConstr.constr -> EConstr.constr -> EConstr.constr val replace : EConstr.constr -> EConstr.constr -> unit Proofview.tactic val general_rewrite : orientation -> Locus.occurrences -> freeze_evars_flag -> dep_proof_flag -> |