Plus de nom commencant par '_' en V8

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4513 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 10 insertions, 8 deletions

diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4
index 3137a38ad..6320a429d 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 = "_eg_"
+let equality_hyp_string = "H_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,6 +276,7 @@ type mimickinfo =
 
   \end{itemize}
 *)
+let heq_prefix = "H_eq_"
 
 type kind_of_hyp = Var | Eq  (*| Rec*)
 
@@ -320,7 +321,7 @@ let rec proofPrinc (mi:mimickinfo) lst_vars lst_eqs lst_recs:
         let lnme,lappel_rec,llevar,llposeq = collect_fix (n+1) in
         (nme::lnme),(appel_rec::lappel_rec),(levar@llevar), (lposeq@llposeq) in
      let lnme,lappel_rec,llevar,llposeq =collect_fix  0 in
-     let lnme' = List.map (fun nme -> newname_append nme   "_ind") lnme in
+     let lnme' = List.map (fun nme -> newname_append nme "_ind") lnme in
      let anme = Array.of_list lnme' in
      let aappel_rec = Array.of_list lappel_rec in
      mkFix((iarr,i),(anme, pisarr,aappel_rec)),llevar,llposeq,evararr,pisarr
@@ -362,13 +363,13 @@ let rec proofPrinc (mi:mimickinfo) lst_vars lst_eqs lst_recs:
       let a',a'' = decompose_lam_n nargs eltPt' in
       let newa'' = 
        if mi.doeqs 
-       then mkLambda (name_of_string "_eq_",lift nargs neweq,lift 1 a'') 
+       then mkLambda (name_of_string heq_prefix,lift nargs neweq,lift 1 a'') 
        else a'' in
       let newmimick = lamn nargs a' newa'' in
       let b',b'' = decompose_prod_n nargs concl_dummy in
       let newb'' = 
        if mi.doeqs 
-       then mkProd (name_of_string "_eq_",lift nargs neweq,lift 1 b'')
+       then mkProd (name_of_string heq_prefix,lift nargs neweq,lift 1 b'')
        else b'' in
       let newconcl = prodn nargs b' newb'' in
       let newmi = {mi with mimick=newmimick; concl=newconcl} in
@@ -514,7 +515,7 @@ let invfun_proof fonc def_fonc gl_abstr pis env sigma =
  princ_proof,levar,lposeq,evararr,absc
 
 (* Do intros [i] times, then do rewrite on all introduced hyps which are called
-   ["_eq_xx"], FIX: have another filter than the name. *)
+   ["H_eq_xx"], FIX: have another filter than the name. *)
 let rec iterintro i = 
  if i<=0 then tclIDTAC else 
    tclTHEN
@@ -527,15 +528,16 @@ let rec iterintro i =
        (fun hyp -> 
         let hypname = (string_of_id (destVar hyp)) in
         let sub = 
-         try String.sub hypname 0 4 with _ -> "" (* different than "_eq_" *) in
-        if sub="_eq_" then rewriteLR hyp else tclFAIL 0 "Cannot rewrite")
+         try String.sub hypname 0 (String.length heq_prefix)
+         with _ -> "" (* different than "H_eq_"*) in
+        if sub=heq_prefix then rewriteLR hyp else tclFAIL 0 "Cannot rewrite")
       )) gl)
 
 
 (* 
        (fun hyp gl -> 
         let _ = print_string ("nthhyp= "^ string_of_int i) in
-        if isConst hyp && ((name_of_const hyp)=="_eq_") then
+        if isConst hyp && ((name_of_const hyp)==heq_prefix) then
           let _ = print_string "YES\n" in
           rewriteLR hyp gl 
         else