From bfc03c53882d7334e4fb327362c354397a8462ba Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 26 Oct 2008 19:22:27 +0000
Subject: Fixes and refinements regarding occurrence selection: - make the
 modifiers "value of" and "type of" for "set" working (it was not!), - clear
 unselected hypotheses in the "in" clause of "induction/destruct" when   the
 destructed term is a variable (experimental), - support for generalization of
 hypotheses in the induction hypotheses using   the "in" clause of "induction"
 (e.g. "induction n in m, H" will   generalize over m -- would it be better to
 have an explicit   "over"/"generalizing" clause ?). Added clause "as" to
 "apply in".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11509 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/tacexpr.ml | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

(limited to 'proofs')

diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 29d7a7bb17..b6be71ea0f 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -58,12 +58,7 @@ let make_red_flag =
   add_flag
     {rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []} 
 
-type hyp_location_flag = (* To distinguish body and type of local defs *)
-  | InHyp
-  | InHypTypeOnly
-  | InHypValueOnly
-
-type 'a raw_hyp_location = 'a with_occurrences * hyp_location_flag
+type 'a raw_hyp_location = 'a with_occurrences * Termops.hyp_location_flag
 
 type 'id move_location =
   | MoveAfter of 'id
-- 
cgit v1.2.3