diff options
| author | Pierre-Marie Pédrot | 2018-06-18 14:32:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-06-18 14:46:09 +0200 |
| commit | 1bbeba35eb385f813a0e4b6d25a437f9bab8191b (patch) | |
| tree | 654b722111fe371722b49c1f52a5ee0e2baf1e24 /src/tac2expr.mli | |
| parent | 1103a3f909b070a54d8fe2765b274aa7d217ec91 (diff) | |
Fixing a batch of deprecation warnings.
Diffstat (limited to 'src/tac2expr.mli')
| -rw-r--r-- | src/tac2expr.mli | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/tac2expr.mli b/src/tac2expr.mli index ddffd13a31..1f2c3ebf3b 100644 --- a/src/tac2expr.mli +++ b/src/tac2expr.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Loc open Names open Libnames @@ -78,7 +77,7 @@ type glb_typedef = type type_scheme = int * int glb_typexpr -type raw_quant_typedef = Misctypes.lident list * raw_typedef +type raw_quant_typedef = Names.lident list * raw_typedef type glb_quant_typedef = int * glb_typedef (** {5 Term syntax} *) @@ -159,11 +158,11 @@ type sexpr = (** {5 Toplevel statements} *) type strexpr = -| StrVal of mutable_flag * rec_flag * (Misctypes.lname * raw_tacexpr) list +| 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 (** Type definition *) -| StrPrm of Misctypes.lident * raw_typexpr * ml_tactic_name +| StrPrm of Names.lident * raw_typexpr * ml_tactic_name (** External definition *) | StrSyn of sexpr list * int option * raw_tacexpr (** Syntactic extensions *) |