diff options
| author | Gaëtan Gilbert | 2018-10-19 21:08:15 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-16 14:56:16 +0100 |
| commit | fc404f718ff960a331f2b9245bb387691be3e7ac (patch) | |
| tree | fc88e38352aaed2a9c052a07f2f614f1fc7196ec /interp/declare.ml | |
| parent | 86bf9da9ef88a0bc82f9d0527b01e424851f4f61 (diff) | |
No Projection.constant in projection <-> constant declaration
Enabled by previous commit about Heads.
Diffstat (limited to 'interp/declare.ml')
| -rw-r--r-- | interp/declare.ml | 9 |
1 files changed, 4 insertions, 5 deletions
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 |