diff options
| author | Maxime Dénès | 2018-06-18 14:21:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-06-18 17:14:24 +0200 |
| commit | eba6d1ffe7a3aa775e6a4984914461364149573f (patch) | |
| tree | 43fe81addd3a3d55968b9e15a29a0332155491ad /src/tac2expr.mli | |
| parent | 15010cea58df81a3ccfdd5a4b2a01375e34853f3 (diff) | |
Adapt to Coq's PR #7797 (removal of reference).
Diffstat (limited to 'src/tac2expr.mli')
| -rw-r--r-- | src/tac2expr.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/tac2expr.mli b/src/tac2expr.mli index 1f2c3ebf3b..1069d0bfa3 100644 --- a/src/tac2expr.mli +++ b/src/tac2expr.mli @@ -26,7 +26,7 @@ type tacref = | TacAlias of ltac_alias type 'a or_relid = -| RelId of qualid CAst.t +| RelId of qualid | AbsKn of 'a (** {5 Misc} *) @@ -160,13 +160,13 @@ type sexpr = type strexpr = | StrVal of mutable_flag * rec_flag * (Names.lname * raw_tacexpr) list (** Term definition *) -| StrTyp of rec_flag * (qualid CAst.t * redef_flag * raw_quant_typedef) list +| StrTyp of rec_flag * (qualid * redef_flag * raw_quant_typedef) list (** Type definition *) | StrPrm of Names.lident * raw_typexpr * ml_tactic_name (** External definition *) | StrSyn of sexpr list * int option * raw_tacexpr (** Syntactic extensions *) -| StrMut of qualid CAst.t * raw_tacexpr +| StrMut of qualid * raw_tacexpr (** Redefinition of mutable globals *) | StrRun of raw_tacexpr (** Toplevel evaluation of an expression *) |