diff options
| author | Pierre-Marie Pédrot | 2017-05-15 15:57:01 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-05-19 15:17:31 +0200 |
| commit | a16d9c10b874a38fd4901e7d946d975ad49592c5 (patch) | |
| tree | 4e328a16062cf93fb1b12c24e4e626738797547b /tac2expr.mli | |
| parent | c341a00d916c27b75c79c2fdcce13e969772a990 (diff) | |
Introducing tactic notations in Ltac2.
Diffstat (limited to 'tac2expr.mli')
| -rw-r--r-- | tac2expr.mli | 21 |
1 files changed, 20 insertions, 1 deletions
diff --git a/tac2expr.mli b/tac2expr.mli index 63207ac78f..acdad9bab4 100644 --- a/tac2expr.mli +++ b/tac2expr.mli @@ -129,7 +129,23 @@ type glb_tacexpr = | GTacExt of glob_generic_argument | GTacPrm of ml_tactic_name * glb_tacexpr list -(** Toplevel statements *) +(** {5 Parsing & Printing} *) + +type exp_level = +| E5 +| E4 +| E3 +| E2 +| E1 +| E0 + +type sexpr = +| SexprStr of string located +| SexprInt of int located +| SexprRec of Loc.t * Id.t option located * sexpr list + +(** {5 Toplevel statements} *) + type strexpr = | StrVal of rec_flag * (Name.t located * raw_tacexpr) list (** Term definition *) @@ -137,6 +153,9 @@ type strexpr = (** Type definition *) | StrPrm of Id.t located * raw_typexpr * ml_tactic_name (** External definition *) +| StrSyn of sexpr list * int option * raw_tacexpr + (** Syntactic extensions *) + (** {5 Dynamic semantics} *) |