From 6ace746e3f49f466591558eaefb001f5948d63fb Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 27 Nov 2003 19:04:44 +0000
Subject: Retour des _eq en v8

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5010 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/funind/tacinv.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4
index 162ea2ebf2..cff2dba1fd 100644
--- a/contrib/funind/tacinv.ml4
+++ b/contrib/funind/tacinv.ml4
@@ -49,7 +49,7 @@ let mkthesort = mkProp (* would like to put Type here, but with which index? *)
 
 (*  this is the prefix used to name equality hypothesis generated by
     case analysis*)
-let equality_hyp_string = if !Options.v7 then "_eg_" else "H_eg_"
+let equality_hyp_string = "_eg_"
 
 (* bug de refine: on doit ssavoir sur quelle hypothese on se trouve. valeur
    initiale au debut de l'appel a la fonction proofPrinc: 1. *)
@@ -276,7 +276,7 @@ type mimickinfo =
 
   \end{itemize}
 *)
-let heq_prefix = if !Options.v7 then "_eq_" else "H_eq_"
+let heq_prefix = "_eq_"
 
 type kind_of_hyp = Var | Eq  (*| Rec*)
 
-- 
cgit v1.2.3