diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/recordops.ml | 12 | ||||
| -rw-r--r-- | pretyping/recordops.mli | 2 |
2 files changed, 7 insertions, 7 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 4faa753dfb..fe9b69dbbc 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -106,16 +106,16 @@ let find_projection = function let prim_table = Summary.ref (Cmap_env.empty : Projection.Repr.t Cmap_env.t) ~name:"record-prim-projs" -let load_prim i (_,p) = - prim_table := Cmap_env.add (Projection.Repr.constant p) p !prim_table +let load_prim i (_,(p,c)) = + prim_table := Cmap_env.add c p !prim_table let cache_prim p = load_prim 1 p -let subst_prim (subst,p) = subst_proj_repr subst p +let subst_prim (subst,(p,c)) = subst_proj_repr subst p, subst_constant subst c -let discharge_prim (_,p) = Some (Lib.discharge_proj_repr p) +let discharge_prim (_,(p,c)) = Some (Lib.discharge_proj_repr p, c) -let inPrim : Projection.Repr.t -> obj = +let inPrim : (Projection.Repr.t * Constant.t) -> obj = declare_object { (default_object "PRIMPROJS") with cache_function = cache_prim ; @@ -124,7 +124,7 @@ let inPrim : Projection.Repr.t -> obj = classify_function = (fun x -> Substitute x); discharge_function = discharge_prim } -let declare_primitive_projection p = Lib.add_anonymous_leaf (inPrim p) +let declare_primitive_projection p c = Lib.add_anonymous_leaf (inPrim (p,c)) let is_primitive_projection c = Cmap_env.mem c !prim_table 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 |