diff options
| author | Pierre-Marie Pédrot | 2017-07-26 17:53:04 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-07-26 18:40:15 +0200 |
| commit | 4395637a6471fc95934fe93da671bda68d415a77 (patch) | |
| tree | fd51fbf117afb8dda9f97e1988e437c133ffeaa7 /src/tac2expr.mli | |
| parent | 2a74da7b6f275634fd8ed9c209edc73f2ae15427 (diff) | |
Ensuring that inductive constructors are always capitalized.
Diffstat (limited to 'src/tac2expr.mli')
| -rw-r--r-- | src/tac2expr.mli | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/src/tac2expr.mli b/src/tac2expr.mli index a9f2109cb2..b268e70cb3 100644 --- a/src/tac2expr.mli +++ b/src/tac2expr.mli @@ -70,19 +70,16 @@ type atom = | AtmInt of int | AtmStr of string -type tacref = -| TacConstant of ltac_constant -| TacConstructor of ltac_constructor - (** Tactic expressions *) type raw_patexpr = -| CPatAny of Loc.t +| CPatVar of Name.t located | CPatRef of Loc.t * ltac_constructor or_relid * raw_patexpr list | CPatTup of raw_patexpr list located type raw_tacexpr = | CTacAtm of atom located -| CTacRef of tacref or_relid +| CTacRef of ltac_constant or_relid +| CTacCst of ltac_constructor or_relid | CTacFun of Loc.t * (raw_patexpr * raw_typexpr option) list * raw_tacexpr | CTacApp of Loc.t * raw_tacexpr * raw_tacexpr list | CTacLet of Loc.t * rec_flag * (Name.t located * raw_typexpr option * raw_tacexpr) list * raw_tacexpr |