diff options
Diffstat (limited to 'intf/tacexpr.mli')
| -rw-r--r-- | intf/tacexpr.mli | 21 |
1 files changed, 2 insertions, 19 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 16ba9f95e..d8e340d1e 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -10,15 +10,13 @@ open Names open Topconstr open Libnames open Nametab -open Glob_term -open Errors -open Pp -open Util +open Genredexpr open Genarg open Pattern open Decl_kinds open Misctypes open Locus +open Pp type 'a or_metaid = AI of 'a | MetaId of loc * string @@ -33,21 +31,6 @@ type letin_flag = bool (* true = use local def false = use Leibniz *) type debug = Debug | Info | Off (* for trivial / auto / eauto ... *) -type glob_red_flag = - | FBeta - | FIota - | FZeta - | FConst of reference or_by_notation list - | FDeltaBut of reference or_by_notation list - -type 'a raw_hyp_location = 'a with_occurrences * hyp_location_flag - -type 'id move_location = - | MoveAfter of 'id - | MoveBefore of 'id - | MoveFirst - | MoveLast (* can be seen as "no move" when doing intro *) - type 'a induction_arg = | ElimOnConstr of 'a | ElimOnIdent of identifier located |