aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/tacexpr.mli
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-05-29 11:08:44 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-05-29 11:08:44 +0000
commita936f2e879ac1f9b2e7e9d8a5376469e3d53c606 (patch)
tree7f0972729eb41828ad9abbaf0dc61ce2366ef870 /intf/tacexpr.mli
parentb31b48407a9f5d36cefd6dec3ddf3e0b8391f14c (diff)
Glob_term now mli-only, operations now in Glob_ops
Stuff about reductions now in genredexpr.mli, operations in redops.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15374 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'intf/tacexpr.mli')
-rw-r--r--intf/tacexpr.mli21
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