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 +
 pretyping/tacred.ml | 7 +++----
 3 files changed, 9 insertions(+), 5 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)
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
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 99776367bb..de87e5029a 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -214,8 +214,7 @@ let invert_name labs l na0 env sigma ref = function
 	  | EvalRel _ | EvalEvar _ -> None
 	  | EvalVar id' -> Some (EvalVar id)
 	  | EvalConst kn ->
-	      let (mp,dp,_) = repr_con kn in
-	      Some (EvalConst (make_con mp dp (label_of_id id))) in
+	      Some (EvalConst (con_with_label kn (label_of_id id))) in
 	match refi with
 	  | None -> None
 	  | Some ref ->
@@ -468,7 +467,6 @@ let reduce_mind_case_use_function func env sigma mia =
     | CoFix (bodynum,(names,_,_) as cofix) ->
 	let build_cofix_name =
 	  if isConst func then
-	    let (mp,dp,_) = repr_con (destConst func) in
             let minargs = List.length mia.mcargs in
 	    fun i ->
 	      if i = bodynum then Some (minargs,func)
@@ -479,7 +477,8 @@ let reduce_mind_case_use_function func env sigma mia =
 		       mutual inductive, try to reuse the global name if
 		       the block was indeed initially built as a global
 		       definition *)
-		    let kn = make_con mp dp (label_of_id id) in
+		    let kn = con_with_label (destConst func) (label_of_id id)
+		    in
 		    try match constant_opt_value env kn with
 		      | None -> None
                           (* TODO: check kn is correct *)
-- 
cgit v1.2.3