From b95e86482ffef29ee4a74c0ef6e7ac2d604d9d3e Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 27 Jan 2011 00:39:56 +0000
Subject: 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
---
 kernel/names.ml  | 6 +++++-
 kernel/names.mli | 1 +
 2 files changed, 6 insertions(+), 1 deletion(-)

(limited to 'kernel')

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)
diff --git a/kernel/names.mli b/kernel/names.mli
index b5e71b9d4b..bf1fca87f3 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -143,6 +143,7 @@ val user_con : constant -> kernel_name
 val canonical_con : constant -> kernel_name
 val repr_con : constant -> module_path * dir_path * label
 val eq_constant : constant -> constant -> bool
+val con_with_label : constant -> label -> constant
 
 val string_of_con : constant -> string
 val con_label : constant -> label
-- 
cgit v1.2.3