From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 pretyping/recordops.mli | 20 +++++++++++++-------
 1 file changed, 13 insertions(+), 7 deletions(-)

(limited to 'pretyping/recordops.mli')

diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 1f7b23c0..415b9641 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -10,7 +10,6 @@
 
 open Names
 open Constr
-open Globnames
 
 (** Operations concerning records and canonical structures *)
 
@@ -40,10 +39,17 @@ val lookup_structure : inductive -> struc_typ
 val lookup_projections : inductive -> Constant.t option list
 
 (** raise [Not_found] if not a projection *)
-val find_projection_nparams : global_reference -> int
+val find_projection_nparams : GlobRef.t -> int
 
 (** raise [Not_found] if not a projection *)
-val find_projection : global_reference -> struc_typ
+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 is_primitive_projection : Constant.t -> bool
+
+val find_primitive_projection : Constant.t -> Projection.Repr.t option
 
 (** {6 Canonical structures } *)
 (** A canonical structure declares "canonical" conversion hints between 
@@ -52,7 +58,7 @@ val find_projection : global_reference -> struc_typ
 
 (** A cs_pattern characterizes the form of a component of canonical structure *)
 type cs_pattern =
-    Const_cs of global_reference
+    Const_cs of GlobRef.t
   | Prod_cs
   | Sort_cs of Sorts.family
   | Default_cs
@@ -71,9 +77,9 @@ val cs_pattern_of_constr : Environ.env -> constr -> cs_pattern * int option * co
 
 val pr_cs_pattern : cs_pattern -> Pp.t
 
-val lookup_canonical_conversion : (global_reference * cs_pattern) -> constr * obj_typ
-val declare_canonical_structure : global_reference -> unit
+val lookup_canonical_conversion : (GlobRef.t * cs_pattern) -> constr * obj_typ
+val declare_canonical_structure : GlobRef.t -> unit
 val is_open_canonical_projection :
   Environ.env -> Evd.evar_map -> Reductionops.state -> bool
 val canonical_projections : unit ->
-  ((global_reference * cs_pattern) * obj_typ) list
+  ((GlobRef.t * cs_pattern) * obj_typ) list
-- 
cgit v1.2.3