diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/evar_kinds.ml | 4 | ||||
| -rw-r--r-- | intf/misctypes.ml | 13 | ||||
| -rw-r--r-- | intf/pattern.ml | 5 | ||||
| -rw-r--r-- | intf/vernacexpr.ml | 22 |
4 files changed, 10 insertions, 34 deletions
diff --git a/intf/evar_kinds.ml b/intf/evar_kinds.ml index c5de383b21..c964ecf1f5 100644 --- a/intf/evar_kinds.ml +++ b/intf/evar_kinds.ml @@ -21,6 +21,8 @@ type obligation_definition_status = Define of bool | Expand type matching_var_kind = FirstOrderPatVar of patvar | SecondOrderPatVar of patvar +type subevar_kind = Domain | Codomain | Body + type t = | ImplicitArg of global_reference * (int * Id.t option) * bool (** Force inference *) @@ -34,4 +36,4 @@ type t = | ImpossibleCase | MatchingVar of matching_var_kind | VarInstance of Id.t - | SubEvar of Evar.t + | SubEvar of subevar_kind option * Evar.t diff --git a/intf/misctypes.ml b/intf/misctypes.ml index 9eb6f62cc3..72db3b31cb 100644 --- a/intf/misctypes.ml +++ b/intf/misctypes.ml @@ -142,19 +142,6 @@ type multi = | RepeatStar | RepeatPlus -type 'a core_destruction_arg = - | ElimOnConstr of 'a - | ElimOnIdent of lident - | ElimOnAnonHyp of int - -type 'a destruction_arg = - clear_flag * 'a core_destruction_arg - -type inversion_kind = - | SimpleInversion - | FullInversion - | FullInversionClear - type ('a, 'b) gen_universe_decl = { univdecl_instance : 'a; (* Declared universes *) univdecl_extensible_instance : bool; (* Can new universes be added *) diff --git a/intf/pattern.ml b/intf/pattern.ml index af2347674f..76367b612a 100644 --- a/intf/pattern.ml +++ b/intf/pattern.ml @@ -10,7 +10,6 @@ open Names open Globnames -open Constr open Misctypes (** {5 Patterns} *) @@ -37,8 +36,8 @@ type constr_pattern = | PIf of constr_pattern * constr_pattern * constr_pattern | PCase of case_info_pattern * constr_pattern * constr_pattern * (int * bool list * constr_pattern) list (** index of constructor, nb of args *) - | PFix of fixpoint - | PCoFix of cofixpoint + | PFix of (int array * int) * (Name.t array * constr_pattern array * constr_pattern array) + | PCoFix of int * (Name.t array * constr_pattern array * constr_pattern array) (** Nota : in a [PCase], the array of branches might be shorter than expected, denoting the use of a final "_ => _" branch *) diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index df061bfb72..06f969f19c 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -297,13 +297,9 @@ type inline = type module_ast_inl = module_ast * inline type module_binder = bool option * lident list * module_ast_inl -(** Cumulativity can be set globally, locally or unset locally and it - can not enabled at all. *) -type cumulative_inductive_parsing_flag = - | GlobalCumulativity - | GlobalNonCumulativity - | LocalCumulativity - | LocalNonCumulativity +(** [Some b] if locally enabled/disabled according to [b], [None] if + we should use the global flag. *) +type vernac_cumulative = VernacCumulative | VernacNonCumulative (** {6 The type of vernacular expressions} *) @@ -338,7 +334,7 @@ type nonrec vernac_expr = | VernacExactProof of constr_expr | VernacAssumption of (Decl_kinds.discharge * Decl_kinds.assumption_object_kind) * inline * (ident_decl list * constr_expr) with_coercion list - | VernacInductive of cumulative_inductive_parsing_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list + | VernacInductive of vernac_cumulative option * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of Decl_kinds.discharge * (fixpoint_expr * decl_notation list) list | VernacCoFixpoint of Decl_kinds.discharge * (cofixpoint_expr * decl_notation list) list | VernacScheme of (lident option * scheme) list @@ -409,8 +405,6 @@ type nonrec vernac_expr = | VernacHints of string list * hints_expr | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) * onlyparsing_flag - | VernacDeclareImplicits of reference or_by_notation * - (explicitation * bool * bool) list list | VernacArguments of reference or_by_notation * vernac_argument_status list (* Main arguments status list *) * (Name.t * vernac_implicit_status) list list (* Extra implicit status lists *) * @@ -418,8 +412,6 @@ type nonrec vernac_expr = [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename | `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes | `DefaultImplicits ] list - | VernacArgumentsScope of reference or_by_notation * - scope_name option list | VernacReserve of simple_binder list | VernacGeneralizable of (lident list) option | VernacSetOpacity of (Conv_oracle.level * reference or_by_notation list) @@ -446,7 +438,6 @@ type nonrec vernac_expr = | VernacRestart | VernacUndo of int | VernacUndoTo of int - | VernacBacktrack of int*int*int | VernacFocus of int option | VernacUnfocus | VernacUnfocused @@ -457,8 +448,6 @@ type nonrec vernac_expr = | VernacCheckGuard | VernacProof of Genarg.raw_generic_argument option * section_subset_expr option | VernacProofMode of string - (* Toplevel control *) - | VernacToplevelControl of exn (* For extension *) | VernacExtend of extend_name * Genarg.raw_generic_argument list @@ -508,14 +497,13 @@ type vernac_type = | VtProofMode of string (* Queries are commands assumed to be "pure", that is to say, they don't modify the interpretation state. *) - | VtQuery of vernac_part_of_script * Feedback.route_id + | VtQuery (* To be removed *) | VtMeta | VtUnknown and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) and vernac_start = string * opacity_guarantee * Id.t list and vernac_sideff_type = Id.t list -and vernac_part_of_script = bool and opacity_guarantee = | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) |