Make simpl use the proper constant when folding (mutual) fixpoints

  Before this commit, when simpl was finding the constant name
  for folding some (mutual) fixpoint, this was done via some
  repr_con followed by make_con. Problem: this doesn't preserve
  the canonical part of a Names.constant. For instance the following
  script was buggish:

 Module M.
 Fixpoint foo n := match n with O => O | S n => bar n end
 with bar n := match n with O => O | S n => foo n end.
 End M.

 Module N.
 Include M. (* foo, bar have here "user name" N but "canonical name" M *)
 Eval simpl in (fun x => bar (S x)).
 (* Anomaly: uncaught exception Failure "Cannot print a global reference". *)
 (* since simpl has produce a different bar with both user and canonical N *)

 TODO : check all other uses of make_con in the rest of the sources...

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

1 files changed, 5 insertions, 1 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index d31c4f93fa..d53a7aa300 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -234,7 +234,7 @@ type constructor = inductive * int
 
 let constant_of_kn kn = (kn,kn)
 let constant_of_kn_equiv kn1 kn2 = (kn1,kn2)
-let make_con mp dir l = ((mp,dir,l),(mp,dir,l))
+let make_con mp dir l = constant_of_kn (mp,dir,l)
 let make_con_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l))
 let canonical_con con = snd con
 let user_con con = fst con
@@ -246,6 +246,10 @@ let debug_pr_con con = str "("++ pr_kn (fst con) ++ str ","++ pr_kn (snd con)++
 let eq_constant (_,kn1) (_,kn2) = kn1=kn2
 let debug_string_of_con con =  string_of_kn (fst con)^"'"^string_of_kn (snd con)
 
+let con_with_label ((mp1,dp1,l1),(mp2,dp2,l2) as con) lbl =
+  if lbl = l1 && lbl = l2 then con
+  else ((mp1,dp1,lbl),(mp2,dp2,lbl))
+
 let con_modpath con = modpath (fst con)
 
 let mind_modpath mind = modpath (fst mind)