diff options
| author | Pierre-Marie Pédrot | 2017-11-02 15:56:51 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-11-02 16:23:02 +0100 |
| commit | 7e7964ddcc41363151d95cddd1a68b3dc70bb070 (patch) | |
| tree | 4d74cdc9286c98ba4522306aeadd96f44c37741f /src/tac2expr.mli | |
| parent | 62606e17ff4afe6a897607d45471b7f4d3ef54b8 (diff) | |
Moving pattern type constraints to pattern AST.
Diffstat (limited to 'src/tac2expr.mli')
| -rw-r--r-- | src/tac2expr.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/tac2expr.mli b/src/tac2expr.mli index 89152dffe7..60f10d360f 100644 --- a/src/tac2expr.mli +++ b/src/tac2expr.mli @@ -91,6 +91,7 @@ type atom = type raw_patexpr_r = | CPatVar of Name.t | CPatRef of ltac_constructor or_tuple or_relid * raw_patexpr list +| CPatCnv of raw_patexpr * raw_typexpr and raw_patexpr = raw_patexpr_r located @@ -98,9 +99,9 @@ type raw_tacexpr_r = | CTacAtm of atom | CTacRef of tacref or_relid | CTacCst of ltac_constructor or_tuple or_relid -| CTacFun of (raw_patexpr * raw_typexpr option) list * raw_tacexpr +| CTacFun of raw_patexpr list * raw_tacexpr | CTacApp of raw_tacexpr * raw_tacexpr list -| CTacLet of rec_flag * (raw_patexpr * raw_typexpr option * raw_tacexpr) list * raw_tacexpr +| CTacLet of rec_flag * (raw_patexpr * raw_tacexpr) list * raw_tacexpr | CTacCnv of raw_tacexpr * raw_typexpr | CTacSeq of raw_tacexpr * raw_tacexpr | CTacCse of raw_tacexpr * raw_taccase list |