diff options
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} *) |