diff options
| author | Pierre-Marie Pédrot | 2017-03-16 09:05:04 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-05-19 15:17:31 +0200 |
| commit | c341a00d916c27b75c79c2fdcce13e969772a990 (patch) | |
| tree | bb7b14457f6e7fce4db9c68a4d8e7d26e1444559 /tac2expr.mli | |
| parent | 735ab0a7d2f7afaed0695e014034f4b2d6e287c8 (diff) | |
Allow raw terms to contain references to absolute definitions.
Diffstat (limited to 'tac2expr.mli')
| -rw-r--r-- | tac2expr.mli | 20 |
1 files changed, 14 insertions, 6 deletions
diff --git a/tac2expr.mli b/tac2expr.mli index 1840b567b4..63207ac78f 100644 --- a/tac2expr.mli +++ b/tac2expr.mli @@ -22,6 +22,10 @@ type ltac_constructor = KerName.t type ltac_projection = KerName.t type type_constant = KerName.t +type 'a or_relid = +| RelId of qualid located +| AbsKn of 'a + (** {5 Misc} *) type ml_tactic_name = { @@ -35,7 +39,7 @@ type raw_typexpr = | CTypVar of Name.t located | CTypArrow of Loc.t * raw_typexpr * raw_typexpr | CTypTuple of Loc.t * raw_typexpr list -| CTypRef of Loc.t * qualid located * raw_typexpr list +| CTypRef of Loc.t * type_constant or_relid * raw_typexpr list type raw_typedef = | CTydDef of raw_typexpr option @@ -66,15 +70,19 @@ 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 -| CPatRef of Loc.t * qualid located * raw_patexpr list +| 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 qualid located +| CTacRef of tacref or_relid | CTacFun of Loc.t * (Name.t located * 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 @@ -85,13 +93,13 @@ type raw_tacexpr = | CTacSeq of Loc.t * raw_tacexpr * raw_tacexpr | CTacCse of Loc.t * raw_tacexpr * raw_taccase list | CTacRec of Loc.t * raw_recexpr -| CTacPrj of Loc.t * raw_tacexpr * qualid located -| CTacSet of Loc.t * raw_tacexpr * qualid located * raw_tacexpr +| CTacPrj of Loc.t * raw_tacexpr * ltac_projection or_relid +| CTacSet of Loc.t * raw_tacexpr * ltac_projection or_relid * raw_tacexpr | CTacExt of Loc.t * raw_generic_argument and raw_taccase = raw_patexpr * raw_tacexpr -and raw_recexpr = (qualid located * raw_tacexpr) list +and raw_recexpr = (ltac_projection or_relid * raw_tacexpr) list type case_info = | GCaseTuple of int |