diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-27 00:39:56 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-27 00:39:56 +0000 |
| commit | b95e86482ffef29ee4a74c0ef6e7ac2d604d9d3e (patch) | |
| tree | cb27ab1fcb0234c7ba1ecf3ea7295b018e950a16 /kernel/names.mli | |
| parent | bc2cebecc14bee4a1a486ff0bead87b6fd69d452 (diff) | |
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
Diffstat (limited to 'kernel/names.mli')
| -rw-r--r-- | kernel/names.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/names.mli b/kernel/names.mli index b5e71b9d4..bf1fca87f 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 |