From 010775eba60ea89645792b48a0686ff15c4ebcb5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 25 Oct 2015 18:43:32 +0100
Subject: Pcoq entries are given a proper module.

Entries defined in the Pcoq AST of symbols must be marshallable, because they
are present in the libstack. Yet, CAMLP4/5 entries are not marshallable as
they contain functional values. This is why the Pcoq module used a pair
[string * string] to describe entries. It is obviously type-unsafe, so
we define a new abstract type in its own module. There is a little issue
though, which is that our entries and CAMLP4/5 entries must be kept
synchronized through an association table. The Pcoq module tries to
maintain this invariant.
---
 dev/printers.mllib  | 1 +
 dev/top_printers.ml | 4 ++--
 2 files changed, 3 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index de43efa670..1a2819feb2 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -191,6 +191,7 @@ Pfedit
 Tactic_debug
 Decl_mode
 Ppconstr
+Entry
 Pcoq
 Printer
 Pptactic
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 1d3d711ac7..7b807a343a 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -519,7 +519,7 @@ let _ =
   extend_vernac_command_grammar ("PrintConstr", 0) None
     [GramTerminal "PrintConstr";
       GramNonTerminal
-        (Loc.ghost,ConstrArgType,Aentry ("constr","constr"),
+        (Loc.ghost,ConstrArgType,Aentry (Entry.unsafe_of_name ("constr","constr")),
 	 Some (Names.Id.of_string "c"))]
 
 let _ =
@@ -536,7 +536,7 @@ let _ =
   extend_vernac_command_grammar ("PrintPureConstr", 0) None
     [GramTerminal "PrintPureConstr";
       GramNonTerminal
-        (Loc.ghost,ConstrArgType,Aentry ("constr","constr"),
+        (Loc.ghost,ConstrArgType,Aentry (Entry.unsafe_of_name ("constr","constr")),
 	 Some (Names.Id.of_string "c"))]
 
 (* Setting printer of unbound global reference *)
-- 
cgit v1.2.3