diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/constrexpr.mli | 4 | ||||
| -rw-r--r-- | intf/decl_kinds.mli | 8 | ||||
| -rw-r--r-- | intf/glob_term.mli | 4 | ||||
| -rw-r--r-- | intf/notation_term.mli | 1 | ||||
| -rw-r--r-- | intf/pattern.mli | 1 | ||||
| -rw-r--r-- | intf/vernacexpr.mli | 3 |
6 files changed, 13 insertions, 8 deletions
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index 64bbd1e835..af6aea1644 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -62,13 +62,13 @@ and cases_pattern_notation_substitution = cases_pattern_expr list list (** for recursive notations *) type constr_expr = - | CRef of reference + | CRef of reference * Univ.universe_instance option | CFix of Loc.t * Id.t located * fix_expr list | CCoFix of Loc.t * Id.t located * cofix_expr list | CProdN of Loc.t * binder_expr list * constr_expr | CLambdaN of Loc.t * binder_expr list * constr_expr | CLetIn of Loc.t * Name.t located * constr_expr * constr_expr - | CAppExpl of Loc.t * (proj_flag * reference) * constr_expr list + | CAppExpl of Loc.t * (proj_flag * reference * Univ.universe_instance option) * constr_expr list | CApp of Loc.t * (proj_flag * constr_expr) * (constr_expr * explicitation located option) list | CRecord of Loc.t * constr_expr option * (reference * constr_expr) list diff --git a/intf/decl_kinds.mli b/intf/decl_kinds.mli index 7111fd0555..2ed776c2d6 100644 --- a/intf/decl_kinds.mli +++ b/intf/decl_kinds.mli @@ -12,6 +12,8 @@ type locality = Discharge | Local | Global type binding_kind = Explicit | Implicit +type polymorphic = bool + type theorem_kind = | Theorem | Lemma @@ -45,9 +47,9 @@ type assumption_object_kind = Definitional | Logical | Conjectural Logical | Hypothesis | Axiom *) -type assumption_kind = locality * assumption_object_kind +type assumption_kind = locality * polymorphic * assumption_object_kind -type definition_kind = locality * definition_object_kind +type definition_kind = locality * polymorphic * definition_object_kind (** Kinds used in proofs *) @@ -55,7 +57,7 @@ type goal_object_kind = | DefinitionBody of definition_object_kind | Proof of theorem_kind -type goal_kind = locality * goal_object_kind +type goal_kind = locality * polymorphic * goal_object_kind (** Kinds used in library *) diff --git a/intf/glob_term.mli b/intf/glob_term.mli index 1d200ca79b..d07766e18c 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -28,7 +28,7 @@ type cases_pattern = (** [PatCstr(p,C,l,x)] = "|'C' 'l' as 'x'" *) type glob_constr = - | GRef of (Loc.t * global_reference) + | GRef of (Loc.t * global_reference * Univ.universe_instance option) | GVar of (Loc.t * Id.t) | GEvar of Loc.t * existential_key * glob_constr list option | GPatVar of Loc.t * (bool * patvar) (** Used for patterns only *) @@ -39,7 +39,7 @@ type glob_constr = | GCases of Loc.t * case_style * glob_constr option * tomatch_tuples * cases_clauses (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *) - + | GProj of Loc.t * projection * glob_constr | GLetTuple of Loc.t * Name.t list * (Name.t * glob_constr option) * glob_constr * glob_constr | GIf of Loc.t * glob_constr * (Name.t * glob_constr option) * glob_constr * glob_constr diff --git a/intf/notation_term.mli b/intf/notation_term.mli index daf605ab28..8bb43e96a5 100644 --- a/intf/notation_term.mli +++ b/intf/notation_term.mli @@ -25,6 +25,7 @@ type notation_constr = | NVar of Id.t | NApp of notation_constr * notation_constr list | NHole of Evar_kinds.t * Genarg.glob_generic_argument option + | NProj of projection * notation_constr | NList of Id.t * Id.t * notation_constr * notation_constr * bool (** Part only in [glob_constr] *) | NLambda of Name.t * notation_constr * notation_constr diff --git a/intf/pattern.mli b/intf/pattern.mli index d0ccb2d9b3..4fa5f418d0 100644 --- a/intf/pattern.mli +++ b/intf/pattern.mli @@ -65,6 +65,7 @@ type constr_pattern = | PRel of int | PApp of constr_pattern * constr_pattern array | PSoApp of patvar * constr_pattern list + | PProj of projection * constr_pattern | PLambda of Name.t * constr_pattern * constr_pattern | PProd of Name.t * constr_pattern * constr_pattern | PLetIn of Name.t * constr_pattern * constr_pattern diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 850f06f87b..857f75ed6d 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -289,7 +289,7 @@ type vernac_expr = (* Gallina *) | VernacDefinition of (locality option * definition_object_kind) * lident * definition_expr - | VernacStartTheoremProof of theorem_kind * + | VernacStartTheoremProof of theorem_kind * (lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)) list * bool | VernacEndProof of proof_end @@ -428,6 +428,7 @@ type vernac_expr = (* Flags *) | VernacProgram of vernac_expr + | VernacPolymorphic of bool * vernac_expr | VernacLocal of bool * vernac_expr and located_vernac_expr = Loc.t * vernac_expr |