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 +
 1 file changed, 1 insertion(+)

(limited to 'dev/printers.mllib')

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
-- 
cgit v1.2.3