- Cleaning (unification of ML names, removal of obsolete code,

  reorganization of code) and documentation (in pcoq.mli) of the code
  for parsing extensions (TACTIC/VERNAC/ARGUMENT EXTEND, Tactic
  Notation, Notation); merged the two copies of interp_entry_name to
  avoid they diverge.  
- Added support in Tactic Notation for ne_..._list_sep in general and
  for (ne_)ident_list(_sep) in particular.



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

1 files changed, 1 insertions, 1 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index ed21213ef..4fb56dfd6 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -939,7 +939,7 @@ in
                        | InSet  -> "_rec_nodep"
                        | InType -> "_rect_nodep")
                 ) in
-            let newid = (string_of_id (Pcoq.coerce_global_to_id y))^suffix in
+            let newid = (string_of_id (coerce_reference_to_id y))^suffix in
             let newref = (dummy_loc,id_of_string newid) in
           ((newref,x,y,z)::l1),l2
       | EqualityScheme  x -> l1,(x::l2)