From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 pretyping/recordops.mli | 27 +++++++++++++++++++++------
 1 file changed, 21 insertions(+), 6 deletions(-)

(limited to 'pretyping/recordops.mli')

diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index ea960aa9..8fc430ae 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: recordops.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Names
@@ -22,14 +22,19 @@ open Library
    constructor (the name of which defaults to Build_S) *)
 
 type struc_typ = {
-  s_CONST : constructor; 
+  s_CONST : constructor;
   s_EXPECTEDPARAM : int;
   s_PROJKIND : (name * bool) list;
   s_PROJ : constant option list }
 
-val declare_structure : 
+val declare_structure :
   inductive * constructor * (name * bool) list * constant option list -> unit
 
+(* [lookup_structure isp] returns the struc_typ associated to the
+   inductive path [isp] if it corresponds to a structure, otherwise
+   it fails with [Not_found] *)
+val lookup_structure : inductive -> struc_typ
+
 (* [lookup_projections isp] returns the projections associated to the
    inductive path [isp] if it corresponds to a structure, otherwise
    it fails with [Not_found] *)
@@ -41,13 +46,22 @@ 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
+
 (*s A canonical structure declares "canonical" conversion hints between *)
 (*  the effective components of a structure and the projections of the  *)
 (*  structure *)
 
 type cs_pattern =
     Const_cs of global_reference
-  | Prod_cs 
+  | Prod_cs
   | Sort_cs of sorts_family
   | Default_cs
 
@@ -60,10 +74,11 @@ type obj_typ = {
   o_TCOMPS : constr list } (* ordered *)
 
 val cs_pattern_of_constr : constr -> cs_pattern * int * constr list
- 
+val pr_cs_pattern : cs_pattern -> Pp.std_ppcmds
+
 val lookup_canonical_conversion : (global_reference * cs_pattern) -> obj_typ
 val declare_canonical_structure : global_reference -> unit
 val is_open_canonical_projection :
   Evd.evar_map -> (constr * constr list) -> bool
-val canonical_projections : unit -> 
+val canonical_projections : unit ->
   ((global_reference * cs_pattern) * obj_typ) list
-- 
cgit v1.2.3