Apply suggestions from code review

Makefile.coq.local

@@ -17,7 +17,7 @@ install-extra::
 	df="`$(COQMKFILE) -destination-of theories/elpi.vo $(COQLIBS)`";\
 	install -m 0644 elpi-builtin.elpi "$(COQLIBINSTALL)/$$df";\
 	install -m 0644 coq-builtin.elpi "$(COQLIBINSTALL)/$$df";\
-	install -m 0644 coq-builtin-parsing-phase.elpi "$(COQLIBINSTALL)/$$df";\
+	install -m 0644 coq-builtin-synterp.elpi "$(COQLIBINSTALL)/$$df";\
 	install -m 0644 elpi/coq-lib.elpi "$(COQLIBINSTALL)/$$df";\
 	install -m 0644 elpi/elpi_elaborator.elpi "$(COQLIBINSTALL)/$$df"
 

apps/NES/elpi/nes_synterp.elpi

@@ -6,9 +6,6 @@ ns->modpath (ns _ M) M.
 pred open-ns->string i:prop, o:string.
 open-ns->string (open-ns S _) S.
 
-pred mk-fresh i:string, o:string.
-mk-fresh NS Fresh :- Fresh is NS ^ "_aux_" ^ {std.any->string {new_int} }.
-
 pred begin-ns i:string, i:list string, i:list prop, o:list prop.
 begin-ns NS Path In Out :-
   if (Path = [])
@@ -170,13 +167,5 @@ resolve.walk S Ctx SP Path :- std.do! [
 pred resolve.err i:string.
 resolve.err S :- coq.error "NES: Namespace not found:" S.
 
-% % The (closed) namespace [NS] containing global [GR], or [].
-% pred gref->path i:gref, o:list string.
-% gref->path GR NS :- std.do! [
-%   coq.gref->path GR MP,
-%   if (gref->path.aux MP NS) true (NS = []),
-% ].
-% pred gref->path.aux i:list string, o:list string.
-% gref->path.aux MP NS :- ns NS M, coq.modpath->path M MP, !.
 
 }

apps/NES/tests/test_NES.v

@@ -11,7 +11,6 @@ Fail NES.Begin "A._.B".
 
 (* name space creation *)
 NES.Begin Foo.
-#[synterp] Elpi Print NES.End.
 Definition x := 3.
 NES.End Foo.
 Print Foo.x.