diff options
Diffstat (limited to 'toplevel/vernacexpr.ml')
| -rw-r--r-- | toplevel/vernacexpr.ml | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 972d7ed9..9d514622 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 9017 2006-07-05 17:27:34Z herbelin $ i*) +(*i $Id: vernacexpr.ml 9154 2006-09-20 17:18:18Z corbinea $ i*) open Util open Names @@ -99,6 +99,7 @@ type showable = | ShowProofNames | ShowIntros of bool | ShowMatch of lident + | ShowThesis | ExplainProof of int list | ExplainTree of int list @@ -146,8 +147,7 @@ type simple_binder = lident list * constr_expr type 'a with_coercion = coercion_flag * 'a type constructor_expr = (lident * constr_expr) with_coercion type inductive_expr = - lident * decl_notation * local_binder list * constr_expr - * constructor_expr list + 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 @@ -195,9 +195,9 @@ type vernac_expr = | VernacEndProof of proof_end | VernacExactProof of constr_expr | VernacAssumption of assumption_kind * simple_binder with_coercion list - | VernacInductive of inductive_flag * inductive_expr list + | VernacInductive of inductive_flag * (inductive_expr * decl_notation) list | VernacFixpoint of (fixpoint_expr * decl_notation) list * bool - | VernacCoFixpoint of cofixpoint_expr list * bool + | VernacCoFixpoint of (cofixpoint_expr * decl_notation) list * bool | VernacScheme of (lident * bool * lreference * sort_expr) list (* Gallina extensions *) @@ -223,9 +223,17 @@ type vernac_expr = module_binder list * module_type_ast option (* Solving *) + | VernacSolve of int * raw_tactic_expr * bool | VernacSolveExistential of int * constr_expr + (* Proof Mode *) + + | VernacDeclProof + | VernacReturn + | VernacProofInstr of Decl_expr.raw_proof_instr + + (* Auxiliary file and library management *) | VernacRequireFrom of export_flag option * specif_flag option * lstring | VernacAddLoadPath of rec_flag * lstring * dir_path option |