diff options
| author | Pierre-Marie Pédrot | 2016-10-25 15:11:41 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-05-19 15:17:31 +0200 |
| commit | 0c3c2459eae24cc8e87c7c6a4a4e6a1afd171d72 (patch) | |
| tree | beea26ffd64058bedf4157e729503b859f8ef2d1 /tac2expr.mli | |
| parent | 94f4ade387013a2e3fe8d1042fbd152088ce1daa (diff) | |
Embedding generic arguments in Ltac2 AST.
Diffstat (limited to 'tac2expr.mli')
| -rw-r--r-- | tac2expr.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/tac2expr.mli b/tac2expr.mli index 445c69aa23..15c630ca87 100644 --- a/tac2expr.mli +++ b/tac2expr.mli @@ -76,6 +76,7 @@ type raw_tacexpr = | CTacCnv of Loc.t * raw_tacexpr * raw_typexpr | CTacSeq of Loc.t * raw_tacexpr * raw_tacexpr | CTacCse of Loc.t * raw_tacexpr * raw_taccase list +| CTacExt of Loc.t * raw_generic_argument and raw_taccase = raw_patexpr * raw_tacexpr @@ -94,6 +95,7 @@ type glb_tacexpr = | GTacArr of glb_tacexpr list | GTacCst of KerName.t * int * glb_tacexpr list | GTacCse of glb_tacexpr * case_info * glb_tacexpr array * (Name.t array * glb_tacexpr) array +| GTacExt of glob_generic_argument | GTacPrm of ml_tactic_name * glb_tacexpr list (** Toplevel statements *) @@ -134,3 +136,5 @@ and closure = { } type ml_tactic = valexpr list -> valexpr Proofview.tactic + +type environment = valexpr Id.Map.t |