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

0 files changed, 0 insertions, 0 deletions