Modules dans COQ\!\!\!\!

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

12 files changed, 581 insertions, 17 deletions

diff --git a/dev/.cvsignore b/dev/.cvsignore
index 6ae156b95f..e494556aa6 100644
--- a/dev/.cvsignore
+++ b/dev/.cvsignore
@@ -1 +1,3 @@
+other
 ocamldebug-v7
+debug_*
\ No newline at end of file
diff --git a/dev/Makefile.common b/dev/Makefile.common
new file mode 100644
index 0000000000..1ff5cf799e
--- /dev/null
+++ b/dev/Makefile.common
@@ -0,0 +1,52 @@
+# this Makefile contains goals common for directory and main devel makefiles
+
+ifndef TOPDIR
+TOPDIR=..
+endif
+
+ifndef BASEDIR
+BASEDIR=
+endif
+
+# the following entries are used to make synchronize two source trees
+# (on big computer and on a laptop for example)
+
+OTHER_FILE=$(TOPDIR)/dev/other
+OTHER=$(shell cat $(OTHER_FILE))
+
+# this is a directory of useful temporary things
+WORKDIR=tmp
+
+ifneq (,$(findstring n,$(MAKEFLAGS)))
+NFLAG=-n
+else
+NFLAG=
+endif
+
+check_other:
+	+@(if [ "$(OTHER)" = "" ] ; then \
+	  echo You must put the ssh path to the other Coq source in $(OTHER_FILE) ; \
+	  echo For example: chrzaszc@ruta:coq/V7 ; \
+	  exit 1; \
+	fi)
+
+get:	check_other
+	+rsync -Cauvz $(NFLAG) $(OTHER)/ $(TOPDIR)/
+	+@(if [ -d $(TOPDIR)/$(WORKDIR) ]; then \
+	  rsync -auvz $(NFLAG) $(OTHER)/tmp/ $(TOPDIR)/tmp/ ; \
+	fi)
+
+put:	check_other
+	+rsync -Cauvz $(NFLAG) $(TOPDIR)/ $(OTHER)/
+	+@(if [ -d $(TOPDIR)/$(WORKDIR) ]; then \
+	  rsync -auvz $(NFLAG) $(TOPDIR)/tmp/ $(OTHER)/tmp/ ; \
+	fi)
+
+sync:	get put
+
+
+conflicts:
+	cvs status | grep File | grep conflicts | less
+
+confl:	conflicts
+
diff --git a/dev/Makefile.devel b/dev/Makefile.devel
new file mode 100644
index 0000000000..78318d59b7
--- /dev/null
+++ b/dev/Makefile.devel
@@ -0,0 +1,46 @@
+# to be linked to makefile (lowercase - takes precedence over Makefile)
+# in main directory
+
+TOPDIR=.
+BASEDIR=
+
+SOURCEDIRS=lib kernel library pretyping parsing proofs tactics toplevel
+
+default:	noargument
+
+# set the devel makefile
+setup-devel:
+	@ln -sfv dev/Makefile.devel makefile
+	@(for i in $(SOURCEDIRS); do \
+	    (cd $(TOPDIR)/$$i; ln -sfv ../dev/Makefile.dir Makefile) \
+	done)
+
+clean-devel:
+	echo rm -f makefile .depend.devel
+	echo rm -f $(foreach dir,$(SOURCEDIRS), $(TOPDIR)/$(dir)/Makefile)
+
+coqtop:	bin/coqtop.byte
+	ln -sf bin/coqtop.byte coqtop
+
+quick: 
+	$(MAKE) states BEST=byte
+
+include Makefile
+
+include $(TOPDIR)/dev/Makefile.common
+
+# this file is better described in dev/Makefile.dir
+include .depend.devel
+
+#if dev/Makefile.local exists, it is included
+ifneq ($(wildcard $(TOPDIR)/dev/Makefile.local),)
+include $(TOPDIR)/dev/Makefile.local
+endif
+
+#runs coqtop with all theories required
+total:
+	ledit ./bin/coqtop.byte $(foreach th,$(THEORIESVO),-require $(notdir $(basename $(th))))
+
+#runs coqtop storing using the history file
+run:	$(TOPDIR)/coqtop
+	ledit -h $(TOPDIR)/dev/debug_history -x $(TOPDIR)/coqtop
diff --git a/dev/Makefile.dir b/dev/Makefile.dir
new file mode 100644
index 0000000000..df205c1f6e
--- /dev/null
+++ b/dev/Makefile.dir
@@ -0,0 +1,102 @@
+# make a link to this file if you are working hard in one directory of Coq
+#   ln -s ../dev/Makefile.dir Makefile
+# if you are working in a sub/dir/ make a link to dev/Makefile.subdir instead
+# this Makefile provides many useful facilities to develop Coq
+# it is not completely compatible with .ml4 files unfortunately
+
+ifndef TOPDIR
+TOPDIR=..
+endif
+
+# this complicated thing should work for subsubdirs as well
+BASEDIR=$(shell (dir=`pwd`; cd $(TOPDIR); top=`pwd`; echo $$dir | sed -e "s|$$top/||"))
+
+noargs:	dir
+
+test-dir:
+	@echo TOPDIR=$(TOPDIR)
+	@echo BASEDIR=$(BASEDIR)
+
+include $(TOPDIR)/dev/Makefile.common
+
+# make this directory
+dir:
+	$(MAKE) -C $(TOPDIR) $(notdir $(BASEDIR))
+
+# make all cmo's in this directory. Useful in case the main Makefile is not
+# up-to-date
+all:	
+	@(for i in *.ml{,4}; do \
+	   echo -n $(BASEDIR)/`basename $$i .ml`.cmo "" ; \
+	done \
+	  | xargs $(MAKE) -C $(TOPDIR) )
+
+# lists all files that should be compiled in this directory
+list:
+	@(for i in *.mli; do \
+	   ls -l `basename $$i .mli`.cmi; \
+	done)
+	@(for i in *.ml{,4}; do \
+	   ls -l `basename $$i .ml`.cmo; \
+	done)
+
+
+clean::  
+	rm -f *.cmi *.cmo *.cmx *.o
+
+# if grammar.cmo files cannot be compiled and main .depend cannot be
+# rebuilt, this is quite useful
+depend:
+	(cd $(TOPDIR); ocamldep -I $(BASEDIR) $(BASEDIR)/*.ml $(BASEDIR)/*.mli > .depend.devel)
+
+# displays the dependency graph of the current directory (vertically,
+# unlike in doc/)
+graph:
+	(ocamldep *.ml *.mli | ocamldot | dot -Tps | gv -) &
+
+
+# the pretty entry draws a dependency graph marking red those nodes
+# which do not have their .cmo files 
+
+.INTERMEDIATE: depend.dot depend.2.dot
+.PHONY: depend.ps
+
+depend.dot:
+	ocamldep *.ml *.mli | ocamldot > $@
+
+depend.2.dot:	depend.dot
+	(i=`cat $< | wc -l`; i=`expr $$i - 1`; head -n $$i $<) > $@
+	(for ml in *.ml; do \
+	   base=`basename $$ml .ml`; \
+	   fst=`echo $$base | cut -c1 | tr [:lower:] [:upper:]`; \
+	   rest=`echo $$base | cut -c2-`; \
+	   name=`echo $$fst $$rest | tr -d " "`; \
+	   cmo=$$base.cmo; \
+	   if [ ! -e $$cmo ]; then \
+	     echo \"$$name\" [color=red]\; >> $@;\
+	   fi;\
+         done;\
+	 echo } >> $@)
+
+depend.ps:	depend.2.dot
+	dot -Tps $< > $@
+
+clean::
+	rm -f depend.ps
+
+pretty:	depend.ps
+	(gv -spartan $<; rm $<) &
+#	gv -spartan $< &
+
+
+# this is not perfect bot mostly WORKS! It just calls the main makefile
+
+%.cmi:	*.mli
+	$(MAKE) -C $(TOPDIR) $(BASEDIR)/$@
+
+SOURCES=$(wildcard *.mli) $(wildcard *.ml) $(wildcard *.ml4)
+%.cmo:	$(SOURCES)
+	$(MAKE) -C $(TOPDIR) $(BASEDIR)/$@
+
+coqtop:	
+	$(MAKE) -C $(TOPDIR) bin/coqtop.byte
diff --git a/dev/Makefile.subdir b/dev/Makefile.subdir
new file mode 100644
index 0000000000..45358c426a
--- /dev/null
+++ b/dev/Makefile.subdir
@@ -0,0 +1,7 @@
+# if you work in a sub/sub-rectory of Coq
+# you should make a link to that makefile 
+#    ln -s ../../dev/Makefile.subdir Makefile
+# in order to have all the facilities of dev/Makefile.dir
+
+TOPDIR=../..
+include $(TOPDIR)/dev/Makefile.dir
diff --git a/dev/base_include b/dev/base_include
index a9d8d78129..83d967ce44 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -6,10 +6,20 @@
 #use "top_printers.ml";;
 
 #install_printer  (* identifier *) prid;;
+#install_printer  (* label *) prlab;;
+#install_printer prmsid;;
+#install_printer prmbid;;
+#install_printer prdir;;
+#install_printer prmp;;
 #install_printer  (* section_path *)  prsp;;
 #install_printer  (* qualid *)  prqualid;;
+#install_printer  (* kernel_name *) prkn;;
 #install_printer  (* constr *)  print_pure_constr;;
 
+(* parsing of names *)
+
+let qid = Libnames.qualid_of_string;;
+
 (* parsing of terms *)
 
 let parse_com   = Pcoq.parse_string Pcoq.Constr.constr;;
@@ -38,7 +48,7 @@ let constr_of_string s =
 open Declarations;;
 
 let constbody_of_string s =
-  let b = Global.lookup_constant (path_of_string s) in
+  let b = Global.lookup_constant (Nametab.locate_constant (qualid_of_sp (path_of_string s))) in
   Util.out_some b.const_body;;
 
 (* Get the current goal *)
diff --git a/dev/changements.txt b/dev/changements.txt
index c75774ee5d..d1df2a810b 100644
--- a/dev/changements.txt
+++ b/dev/changements.txt
@@ -1,3 +1,188 @@
+CHANGES DUE TO INTRODUCTION OF MODULES
+======================================
+
+1.Kernel
+--------
+
+  The module level has no effect on constr except for the structure of
+section_path. The type of unique names for constructions (what
+section_path served) is now called a kernel name and is defined by
+ 
+type uniq_ident = int * string * dir_path (* int may be enough *)
+type module_path =
+  | MPfile of dir_path    (* reference to physical module, e.g. file *)
+  | MPbound of uniq_ident (* reference to a module parameter in a functor *)
+  | MPself of uniq_ident  (* reference to one of the containing module *)
+  | MPdot of module_path * label
+type label = identifier
+type kernel_name = module_path * dir_path * label
+                   ^^^^^^^^^^^   ^^^^^^^^   ^^^^^
+                        |           |         \
+                        |           |          the base name
+                        |           \
+                       /             the (true) section path
+   example:                          (non empty only inside open sections)
+   L = (* i.e. some file of logical name L *)
+   struct
+     module A = struct Def a = ... end
+   end
+   M = (* i.e. some file of logical name M *)
+   struct
+     Def t = ...
+     N = functor (X : sig module T = struct Def b = ... end end) -> struct
+       module O = struct
+         Def u = ...
+       end
+       Def x := ... <M>.t ... <N>.O.u ... X.T.b ... L.A.a
+ 
+   <M> and <N> are self-references, X is a bound reference and L is a
+reference to a physical module.
+ 
+  Notice that functor application is not part of a path: it must be
+named by a "module M = F(A)" declaration to be used in a kernel
+name.
+ 
+  Notice that Jacek chose a practical approach, making directories not
+modules. Another approach could have been to replace the constructor
+MPfile by a constant constructor MProot representing the root of the
+world.
+ 
+  Other relevant informations are in kernel/entries.ml (type
+module_expr) and kernel/declarations.ml (type module_body and
+module_type_body).                                                              
+
+2. Library
+----------
+
+i) tables 
+[Summaries] - the only change is the special treatment of the
+global environmet.
+
+ii) objects 
+[Libobject] declares persistent objects, given with methods:
+
+   * cache_function specifying how to add the object in the current
+       scope;
+   * load_function, specifying what to do when the module 
+       containing the object is loaded; 
+   * open_function, specifying what to do when the module 
+       containing the object is opened (imported);
+   * classify_function, specyfying what to do with the object,
+       when the current module (containing the object) is ended. 
+   * subst_function
+   * export_function, to signal end_section survival
+
+(Almost) Each of these methods is called with a parameter of type
+object_name = section_path * kernel_name
+where section_path is the full user name of the object (such as
+Coq.Init.Datatypes.Fst) and kernel_name is its substitutive internal
+version such as (MPself<Datatypes#1>,[],"Fst") (see above)
+
+
+What happens at the end of an interactive module ?
+==================================================
+(or when a file is stored and reloaded from disk)
+
+All summaries (except Global environment) are reverted to the state
+from before the beginning of the module, and:
+
+a) the objects (again, since last Declaremods.start_module or
+   Library.start_library) are classified using the classify_function.
+   To simplify consider only those who returned Substitute _ or Keep _.
+
+b) If the module is not a functor, the subst_function for each object of
+   the first group is called with the substitution 
+   [MPself "<Datatypes#1>" |-> MPfile "Coq.Init.Datatypes"].
+   Then the load_function is called for substituted objects and the
+   "keep" object. 
+   (If the module is a library the substitution is done at reloading).
+
+c) The objects which returned substitute are stored in the modtab
+   together with the self ident of the module, and functor argument
+   names if the module was a functor.
+
+   They will be used (substituted and loaded) when a command like 
+     Module M := F(N)    or
+     Module Z := N 
+   is evaluated
+
+
+The difference between "substitute" and "keep" objects
+========================================================
+i) The "keep" objects can _only_ reference other objects by section_paths
+and qualids. They do not need the substitution function.
+
+They will work after end_module (or reloading a compiled library),
+because these operations do not change section_path's
+
+They will obviously not work after Module Z:=N.
+ 
+These would typically be grammar rules, pretty printing rules etc.
+
+
+
+ii) The "substitute" objects can _only_ reference objects by
+kernel_names. They must have a valid subst_function. 
+
+They will work after end_module _and_ after Module Z:=N or 
+Module Z:=F(M).
+
+
+
+Other kinds of objects:
+iii) "Dispose" - objects which do not survive end_module
+     As a consequence, objects which reference other objects sometimes
+     by kernel_names and sometimes by section_path must be of this kind...
+
+iv) "Anticipate" - objects which must be treated individually by
+    end_module (typically "REQUIRE" objects)
+
+
+
+Writing subst_thing functions
+=============================
+The subst_thing shoud not copy the thing if it hasn't actually
+changed. There are some cool emacs macros in dev/objects.el 
+to help writing subst functions this way quickly and without errors.
+Also there are *_smartmap functions in Util.
+
+The subst_thing functions are already written for many types,
+including constr (Term.subst_mps), 
+global_reference (Libnames.subst_global),
+rawconstr (Rawterm.subst_raw) etc
+
+They are all (apart from constr, for now) written in the non-copying
+way.
+
+
+Nametab
+=======
+
+Nametab has been made more uniform. For every kind of thing there is
+only one "push" function and one "locate" function. 
+
+
+Lib
+===
+
+library_segment is now a list of object_name * library_item, where
+object_name = section_path * kernel_name (see above)
+
+New items have been added for open modules and module types
+
+
+Declaremods
+==========
+Functions to declare interactive and noninteractive modules and module
+types.
+
+
+Library
+=======
+Uses Declaremods to actually communicate with Global and to register
+objects.
+
+
 MAIN CHANGES FROM COQ V7.3
 ==========================
 
diff --git a/dev/db b/dev/db
index f9a7f8d844..5440ff8f10 100644
--- a/dev/db
+++ b/dev/db
@@ -1,6 +1,12 @@
 load_printer "gramlib.cma"
 load_printer "top_printers.cmo"
 install_printer Top_printers.prid
+install_printer Top_printers.prlab
+install_printer Top_printers.prmsid
+install_printer Top_printers.prmbid
+install_printer Top_printers.prdir
+install_printer Top_printers.prmp
+install_printer Top_printers.prkn
 install_printer Top_printers.prsp
 install_printer Top_printers.prqualid
 install_printer Top_printers.prast
@@ -24,4 +30,5 @@ install_printer Top_printers.prevc
 install_printer Top_printers.prwc
 install_printer Top_printers.prclenv
 
+install_printer Top_printers.pr_obj                                                     
 
diff --git a/dev/include b/dev/include
index 165853221f..84f45fb2ae 100644
--- a/dev/include
+++ b/dev/include
@@ -27,3 +27,4 @@
 #install_printer  (* env *) ppenv;;
 
 #install_printer  (* tactic *) pptac;;
+#install_printer  (* object *) pr_obj;;
diff --git a/dev/objects.el b/dev/objects.el
new file mode 100644
index 0000000000..4e531fd7b1
--- /dev/null
+++ b/dev/objects.el
@@ -0,0 +1,137 @@
+; functions to change old style object declaration to new style
+
+(defun repl-open nil
+  (interactive)
+  (query-replace-regexp 
+   "open_function\\([ 	]*\\)=\\([ 	]*\\)cache_\\([a-zA-Z0-9'_]*\\)\\( *\\);" 
+   "open_function\\1=\\2(fun i o -> if i=1 then cache_\\3 o)\\4;") 
+  )
+
+(global-set-key [f6] 'repl-open)
+
+(defun repl-load nil
+  (interactive)
+  (query-replace-regexp 
+   "load_function\\([ 	]*\\)=\\([ 	]*\\)cache_\\([a-zA-Z0-9'_]*\\)\\( *\\);" 
+   "load_function\\1=\\2(fun _ -> cache_\\3)\\4;") 
+  )
+
+(global-set-key [f7] 'repl-load)
+
+(defun repl-decl nil
+  (interactive)
+  (query-replace-regexp
+   "\\(Libobject\.\\)?declare_object[ 
+	]*([ 	]*\\(.*\\)[ 
+	]*,[ 	]*
+\\([ 	]*\\){\\([ 	]*\\)\\([^ ][^}]*\\)}[ 	]*)"
+
+   "\\1declare_object {(\\1default_object \\2) with
+\\3 \\4\\5}")
+;   "|$1=\\1|$2=\\2|$3=\\3|$4=\\4|")
+)
+
+(global-set-key [f9] 'repl-decl)
+
+; eval the above and try f9 f6 f7 on the following:
+
+let (inThing,outThing) =
+  declare_object
+    ("THING", 
+     { load_function = cache_thing;
+       cache_function = cache_thing;
+       open_function = cache_thing;
+       export_function = (function x -> Some x)
+     })
+
+
+;%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+;%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+; functions helping writing non-copying substitutions
+
+(defun make-subst (name)
+  (interactive "s")
+  (defun f (l)
+    (save-excursion
+      (query-replace-regexp
+       (concat "\\([a-zA-z_0-9]*\\)[ 	]*:[ 	]*" 
+	       (car l) 
+	       "\\([ 	]*;\\|[ 	
+]*\}\\)")
+       (concat "let \\1\' = " (cdr l) " " name "\\1 in"))
+      )
+    )
+  (mapcar 'f '(("constr"."subst_mps subst") 
+	       ("Coqast.t"."subst_ast subst") 
+	       ("Coqast.t list"."list_smartmap (subst_ast subst)") 
+	       ("'pat"."subst_pat subst") 
+	       ("'pat unparsing_hunk"."subst_hunk subst_pat subst")
+	       ("'pat unparsing_hunk list"."list_smartmap (subst_hunk subst_pat subst)") 
+	       ("'pat syntax_entry"."subst_syntax_entry subst_pat subst")
+	       ("'pat syntax_entry list"."list_smartmap (subst_syntax_entry subst_pat subst)") 
+	       ("constr option"."option_smartmap (subst_mps subst)")
+	       ("constr list"."list_smartmap (subst_mps subst)")
+	       ("constr array"."array_smartmap (subst_mps subst)")
+	       ("global_reference"."subst_global subst")
+	       ("extended_global_reference"."subst_ext subst")
+	       ("obj_typ"."subst_obj subst")
+	       )
+	  )
+  )
+
+
+(global-set-key [f2] 'make-subst)
+
+(defun make-if (name)
+  (interactive "s")
+  (save-excursion
+    (query-replace-regexp
+     "\\([a-zA-z_0-9]*\\)[ 	]*:[ 	]*['a-zA-z_. ]*\\(;\\|[ 	
+]*\}\\)"
+     (concat "&& \\1\' == " name "\\1")
+     )
+    )
+  )
+
+(global-set-key [f3] 'make-if)
+
+(defun make-record nil
+  (interactive)
+  (save-excursion 
+    (query-replace-regexp
+     "\\([a-zA-z_0-9]*\\)[ 	]*:[ 	]*['a-zA-z_. ]*\\(;\\|[ 	
+]*\}\\)"
+     (concat "\\1 = \\1\' ;")
+     )
+    )
+  )
+
+(global-set-key [f4] 'make-record)
+
+(defun make-prim nil
+  (interactive)
+  (save-excursion (query-replace-regexp "\\<[a-zA-Z'_0-9]*\\>" "\\&'"))
+  )
+
+(global-set-key [f5] 'make-prim)
+
+
+; eval the above, yank the text below and do 
+; paste f2 morph.
+; paste f3 morph.
+; paste f4
+
+      lem : constr;
+      profil : bool list;
+      arg_types : constr list;
+      lem2 : constr option                                                      }
+
+
+; and you almost get   Setoid_replace.subst_morph  :)
+
+; and now f5 on this:
+
+   (ref,(c1,c2))
+
+
+
diff --git a/dev/ocamldebug-v7.template b/dev/ocamldebug-v7.template
index 115cba72f9..cbb72ce270 100644
--- a/dev/ocamldebug-v7.template
+++ b/dev/ocamldebug-v7.template
@@ -5,9 +5,9 @@
 export COQTOP=COQTOPDIRECTORY
 export COQLIB=COQLIBDIRECTORY
 export COQTH=$COQLIB/theories
-export CAMLP4LIB=CAMLP4LIBDIRECTORY
 CAMLBIN=CAMLBINDIRECTORY
 OCAMLDEBUG=$CAMLBIN/ocamldebug
+export CAMLP4LIB=`$CAMLBIN/camlp4 -where`
 
 args=""
 coqdebug="no"
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 417bbfce2b..0339a8fddd 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -12,6 +12,7 @@ open System
 open Pp
 open Ast
 open Names
+open Libnames
 open Nameops
 open Sign
 open Univ
@@ -39,9 +40,22 @@ let pppattern = (fun x -> pp(pr_pattern x))
 let pptype = (fun x -> pp(prtype x))
 
 let prid id = pp (pr_id id)
+let prlab l = pp (pr_lab l)
+
+let prmsid msid = pp (str (string_of_msid msid))
+let prmbid mbid = pp (str (string_of_mbid mbid))
+
+let prdir dir = pp (pr_dirpath dir)
+
+let prmp mp = pp(str (string_of_mp mp))
+let prkn kn = pp(pr_kn kn)
+
+let prsp sp = pp(pr_sp sp)
+
+let prqualid qid = pp(pr_qualid qid)
 
 let prconst (sp,j) =
-    pp (str"#" ++ pr_sp sp ++ str"=" ++ prterm j.uj_val)
+    pp (str"#" ++ pr_kn sp ++ str"=" ++ prterm j.uj_val)
 
 let prvar ((id,a)) =
     pp (str"#" ++ pr_id id ++ str":" ++ prterm a)
@@ -51,10 +65,6 @@ let genprj f j =
 
 let prj j = pp (genprj prjudge j)
 
-let prsp sp = pp(pr_sp sp)
-
-let prqualid qid = pp(Nametab.pr_qualid qid)
-
 let prgoal g = pp(prgl g)
 
 let prsigmagoal g = pp(prgl (sig_it g))
@@ -81,6 +91,8 @@ let ppenv e = pp (pr_rel_context e (rel_context e))
 
 let pptac = (fun x -> pp(Pptactic.pr_raw_tactic x))
 
+let pr_obj obj = Format.print_string (Libobject.object_tag obj)
+
 let cnt = ref 0
 
 let constr_display csr =
@@ -99,11 +111,11 @@ let constr_display csr =
       ^(term_display t)^","^(term_display c)^")"
   | App (c,l) -> "App("^(term_display c)^","^(array_display l)^")\n"
   | Evar (e,l) -> "Evar("^(string_of_int e)^","^(array_display l)^")"
-  | Const c -> "Const("^(string_of_path c)^")"
+  | Const c -> "Const("^(string_of_kn c)^")"
   | Ind (sp,i) ->
-      "MutInd("^(string_of_path sp)^","^(string_of_int i)^")"
+      "MutInd("^(string_of_kn sp)^","^(string_of_int i)^")"
   | Construct ((sp,i),j) ->
-      "MutConstruct(("^(string_of_path sp)^","^(string_of_int i)^"),"
+      "MutConstruct(("^(string_of_kn sp)^","^(string_of_int i)^"),"
       ^(string_of_int j)^")"
   | Case (ci,p,c,bl) ->
       "MutCase(<abs>,"^(term_display p)^","^(term_display c)^","
@@ -243,13 +255,15 @@ let print_pure_constr csr =
     | Name id -> print_string (string_of_id id)
     | Anonymous -> print_string "_"
 (* Remove the top names for library and Scratch to avoid long names *)
-  and sp_display sp = let ls = 
-    match List.rev (List.map string_of_id (repr_dirpath (dirpath sp))) with 
-        ("Scratch"::l)-> l
-      | ("Coq"::_::l) -> l 
-      | l             -> l
-  in  List.iter (fun x -> print_string x; print_string ".") ls;
-      print_string (string_of_id  (basename sp))
+  and sp_display sp = 
+    let dir,l = decode_kn sp in
+    let ls = 
+      match List.rev (List.map string_of_id (repr_dirpath dir)) with 
+          ("Top"::l)-> l
+	| ("Coq"::_::l) -> l 
+	| l             -> l
+    in  List.iter (fun x -> print_string x; print_string ".") ls;
+      print_string (string_of_id l)
 
   in
      box_display csr; print_flush()
@@ -272,3 +286,4 @@ let _ =
   	      print_pure_constr (Astterm.interp_constr evmap sign c))
        | _ -> bad_vernac_args "PrintPureConstr")
 *)
+