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.
---
 interp/declare.ml | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'interp')

diff --git a/interp/declare.ml b/interp/declare.ml
index a9bfe8cabb..1e972d3e35 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -358,10 +358,6 @@ let inInductive : mutual_inductive_entry -> obj =
 
 let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) =
   let id = Label.to_id label in
-  let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in
-  Recordops.declare_primitive_projection p;
-  (* ^ needs to happen before declaring the constant, otherwise
-     Heads gets confused. *)
   let univs = match univs with
     | Monomorphic_ind_entry _ ->
       (** Global constraints already defined through the inductive *)
@@ -378,7 +374,10 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter
       Vars.subst_instance_constr u term, Vars.subst_instance_constr u types
   in
   let entry = definition_entry ~types ~univs term in
-  ignore(declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent))
+  let cst = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in
+  let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in
+  Recordops.declare_primitive_projection p cst
+
 
 let declare_projections univs mind =
   let env = Global.env () in
-- 
cgit v1.2.3