From fc404f718ff960a331f2b9245bb387691be3e7ac Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 19 Oct 2018 21:08:15 +0200
Subject: No Projection.constant in projection <-> constant declaration

Enabled by previous commit about Heads.
---
 pretyping/recordops.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/recordops.mli')

diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 415b964168..3e43372b65 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -45,7 +45,7 @@ val find_projection_nparams : GlobRef.t -> int
 val find_projection : GlobRef.t -> struc_typ
 
 (** Sets up the mapping from constants to primitive projections *)
-val declare_primitive_projection : Projection.Repr.t -> unit
+val declare_primitive_projection : Projection.Repr.t -> Constant.t -> unit
 
 val is_primitive_projection : Constant.t -> bool
 
-- 
cgit v1.2.3