Imported Upstream version 8.5~beta1+dfsg

1 files changed, 12 insertions, 20 deletions

diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 442e51db..37d5b4c2 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -1,17 +1,14 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 open Names
-open Nametab
 open Term
-open Libnames
-open Libobject
-open Library
+open Globnames
 
 (** Operations concerning records and canonical structures *)
 
@@ -22,11 +19,11 @@ open Library
 type struc_typ = {
   s_CONST : constructor;
   s_EXPECTEDPARAM : int;
-  s_PROJKIND : (name * bool) list;
+  s_PROJKIND : (Name.t * bool) list;
   s_PROJ : constant option list }
 
 type struc_tuple =
-    inductive * constructor * (name * bool) list * constant option list
+    inductive * constructor * (Name.t * bool) list * constant option list
 
 val declare_structure : struc_tuple -> unit
 
@@ -46,20 +43,12 @@ val find_projection_nparams : global_reference -> int
 (** raise [Not_found] if not a projection *)
 val find_projection : global_reference -> struc_typ
 
-(** we keep an index (dnet) of record's arguments + fields
-   (=methods). Here is how to declare them: *)
-val declare_method :
-  global_reference -> Evd.evar -> Evd.evar_map -> unit
-  (** and here is how to search for methods matched by a given term: *)
-val methods_matching : constr ->
-  ((global_reference*Evd.evar*Evd.evar_map) *
-     (constr*existential_key)*Termops.subst) list
-
 (** {6 Canonical structures } *)
 (** A canonical structure declares "canonical" conversion hints between 
     the effective components of a structure and the projections of the  
     structure *)
 
+(** A cs_pattern characterizes the form of a component of canonical structure *)
 type cs_pattern =
     Const_cs of global_reference
   | Prod_cs
@@ -68,18 +57,21 @@ type cs_pattern =
 
 type obj_typ = {
   o_DEF : constr;
-  o_INJ : int;      (** position of trivial argument *)
+  o_CTX : Univ.ContextSet.t;
+  o_INJ : int option;      (** position of trivial argument *)
   o_TABS : constr list;    (** ordered *)
   o_TPARAMS : constr list; (** ordered *)
   o_NPARAMS : int;
   o_TCOMPS : constr list } (** ordered *)
 
-val cs_pattern_of_constr : constr -> cs_pattern * int * constr list
+(** Return the form of the component of a canonical structure *)
+val cs_pattern_of_constr : constr -> cs_pattern * int option * constr list
+
 val pr_cs_pattern : cs_pattern -> Pp.std_ppcmds
 
-val lookup_canonical_conversion : (global_reference * cs_pattern) -> obj_typ
+val lookup_canonical_conversion : (global_reference * cs_pattern) -> constr * obj_typ
 val declare_canonical_structure : global_reference -> unit
 val is_open_canonical_projection :
-  Environ.env -> Evd.evar_map -> (constr * constr list) -> bool
+  Environ.env -> Evd.evar_map -> (constr * constr Reductionops.Stack.t) -> bool
 val canonical_projections : unit ->
   ((global_reference * cs_pattern) * obj_typ) list