From 49356f9dd870d7d42e1e4ffbfc00906832197ef1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 9 Nov 2003 15:16:46 +0000
Subject: Traduction semantique des InHyp de clause en InHypValue si local def

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

(limited to 'proofs')

diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 7ded6b4c92..5de120dbbb 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -50,9 +50,13 @@ let make_red_flag =
   add_flag
     {rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []} 
 
-type 'a raw_hyp_location = (* To distinguish body and type of local defs *)
-  | InHyp of 'a
-  | InHypType of 'a
+type hyp_location_flag = (* To distinguish body and type of local defs *)
+  | InHyp
+  | InHypTypeOnly
+  | InHypValueOnly
+
+type 'a raw_hyp_location = 
+    'a * (hyp_location_flag * hyp_location_flag option ref)
 
 type 'a induction_arg =
   | ElimOnConstr of 'a
-- 
cgit v1.2.3