summaryrefslogtreecommitdiff
path: root/toplevel/vernacexpr.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /toplevel/vernacexpr.ml
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'toplevel/vernacexpr.ml')
-rw-r--r--toplevel/vernacexpr.ml65
1 files changed, 49 insertions, 16 deletions
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 9f51841d..744c3a6f 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: vernacexpr.ml 10067 2007-08-09 17:13:16Z msozeau $ i*)
+(*i $Id: vernacexpr.ml 11024 2008-05-30 12:41:39Z msozeau $ i*)
open Util
open Names
@@ -37,7 +37,7 @@ type printable =
| PrintFullContext
| PrintSectionContext of reference
| PrintInspect of int
- | PrintGrammar of string * string
+ | PrintGrammar of string
| PrintLoadPath
| PrintModules
| PrintModule of reference
@@ -48,6 +48,8 @@ type printable =
| PrintOpaqueName of reference
| PrintGraph
| PrintClasses
+ | PrintTypeClasses
+ | PrintInstances of reference
| PrintLtac of reference
| PrintCoercions
| PrintCoercionPaths of class_rawexpr * class_rawexpr
@@ -64,6 +66,7 @@ type printable =
| PrintVisibility of string option
| PrintAbout of reference
| PrintImplicit of reference
+ | PrintAssumptions of reference
type search_about_item =
| SearchRef of reference
@@ -109,7 +112,7 @@ type comment =
| CommentInt of int
type hints =
- | HintsResolve of constr_expr list
+ | HintsResolve of (int option * constr_expr) list
| HintsImmediate of constr_expr list
| HintsUnfold of reference list
| HintsConstructors of reference list
@@ -144,10 +147,12 @@ type sort_expr = Rawterm.rawsort
type decl_notation = (string * constr_expr * scope_name option) option
type simple_binder = lident list * constr_expr
+type class_binder = lident * constr_expr list
type 'a with_coercion = coercion_flag * 'a
type constructor_expr = (lident * constr_expr) with_coercion
type inductive_expr =
lident * local_binder list * constr_expr * constructor_expr list
+
type definition_expr =
| ProveBody of local_binder list * constr_expr
| DefineBody of local_binder list * raw_red_expr option * constr_expr
@@ -167,12 +172,15 @@ type proof_end =
| Admitted
| Proved of opacity_flag * (lident * theorem_kind option) option
+type scheme =
+ | InductionScheme of bool * lreference * sort_expr
+ | EqualityScheme of lreference
+
type vernac_expr =
(* Control *)
| VernacList of located_vernac_expr list
| VernacLoad of verbose_flag * lstring
| VernacTime of vernac_expr
- | VernacVar of lident
(* Syntax *)
| VernacTacticNotation of int * grammar_production list * raw_tactic_expr
@@ -190,15 +198,16 @@ type vernac_expr =
(* Gallina *)
| VernacDefinition of definition_kind * lident * definition_expr *
declaration_hook
- | VernacStartTheoremProof of theorem_kind * lident *
- (local_binder list * constr_expr) * bool * declaration_hook
+ | VernacStartTheoremProof of theorem_kind *
+ (lident option * (local_binder list * constr_expr)) list *
+ bool * declaration_hook
| VernacEndProof of proof_end
| VernacExactProof of constr_expr
- | VernacAssumption of assumption_kind * simple_binder with_coercion list
+ | VernacAssumption of assumption_kind * bool * simple_binder with_coercion list
| VernacInductive of inductive_flag * (inductive_expr * decl_notation) list
| VernacFixpoint of (fixpoint_expr * decl_notation) list * bool
| VernacCoFixpoint of (cofixpoint_expr * decl_notation) list * bool
- | VernacScheme of (lident * bool * lreference * sort_expr) list
+ | VernacScheme of (lident option * scheme) list
| VernacCombinedScheme of lident * lident list
(* Gallina extensions *)
@@ -211,10 +220,30 @@ type vernac_expr =
export_flag option * specif_flag option * lreference list
| VernacImport of export_flag * lreference list
| VernacCanonical of lreference
- | VernacCoercion of strength * lreference * class_rawexpr * class_rawexpr
- | VernacIdentityCoercion of strength * lident *
+ | VernacCoercion of locality * lreference * class_rawexpr * class_rawexpr
+ | VernacIdentityCoercion of locality * lident *
class_rawexpr * class_rawexpr
+ (* Type classes *)
+ | VernacClass of
+ lident * (* name *)
+ local_binder list * (* params *)
+ sort_expr located option * (* arity *)
+ local_binder list * (* constraints *)
+ (lident * bool * constr_expr) list (* props, with substructure hints *)
+
+ | VernacInstance of
+ bool * (* global *)
+ local_binder list * (* super *)
+ typeclass_constraint * (* instance name, class name, params *)
+ (lident * lident list * constr_expr) list * (* props *)
+ int option (* Priority *)
+
+ | VernacContext of typeclass_context
+
+ | VernacDeclareInstance of
+ lident (* instance name *)
+
(* Modules and Module Types *)
| VernacDeclareModule of bool option * lident *
module_binder list * (module_type_ast * bool)
@@ -222,6 +251,7 @@ type vernac_expr =
module_binder list * (module_type_ast * bool) option * module_ast option
| VernacDeclareModuleType of lident *
module_binder list * module_type_ast option
+ | VernacInclude of include_ast
(* Solving *)
@@ -248,6 +278,7 @@ type vernac_expr =
| VernacRestoreState of lstring
(* Resetting *)
+ | VernacRemoveName of lident
| VernacResetName of lident
| VernacResetInitial
| VernacBack of int
@@ -255,14 +286,15 @@ type vernac_expr =
(* Commands *)
| VernacDeclareTacticDefinition of
- rec_flag * (lident * raw_tactic_expr) list
+ rec_flag * (reference * bool * raw_tactic_expr) list
| VernacHints of locality_flag * lstring list * hints
- | VernacSyntacticDefinition of identifier * constr_expr * locality_flag *
- onlyparsing_flag
- | VernacDeclareImplicits of locality_flag * lreference *
- explicitation list option
+ | VernacSyntacticDefinition of identifier located * (identifier list * constr_expr) *
+ locality_flag * onlyparsing_flag
+ | VernacDeclareImplicits of locality_flag * lreference *
+ (explicitation * bool * bool) list option
| VernacReserve of lident list * constr_expr
- | VernacSetOpacity of opacity_flag * lreference list
+ | VernacSetOpacity of
+ locality_flag * (Conv_oracle.level * lreference list) list
| VernacUnsetOption of Goptions.option_name
| VernacSetOption of Goptions.option_name * option_value
| VernacAddOption of Goptions.option_name * option_ref_value list
@@ -285,6 +317,7 @@ type vernac_expr =
| VernacSuspend
| VernacResume of lident option
| VernacUndo of int
+ | VernacUndoTo of int
| VernacBacktrack of int*int*int
| VernacFocus of int option
| VernacUnfocus