added products and sorts as possible heads for canonical structures

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10577 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 11 insertions, 3 deletions

diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 321584b5b..348407ae1 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -36,14 +36,22 @@ val find_projection_nparams : global_reference -> int
 (*  the effective components of a structure and the projections of the  *)
 (*  structure *)
 
+type cs_pattern =
+    Const_cs of global_reference
+  | Prod_cs 
+  | Sort_cs of sorts_family
+  | Default_cs
+
 type obj_typ = {
   o_DEF : constr;
   o_INJ : int;      (* position of trivial argument *)
   o_TABS : constr list;    (* ordered *)
   o_TPARAMS : constr list; (* ordered *)
   o_TCOMPS : constr list } (* ordered *)
-               
-val lookup_canonical_conversion : (global_reference * global_reference option) -> obj_typ
+
+val cs_pattern_of_constr : constr -> cs_pattern * int * constr list
+ 
+val lookup_canonical_conversion : (global_reference * cs_pattern) -> obj_typ
 val declare_canonical_structure : global_reference -> unit
 val canonical_projections : unit -> 
-  ((global_reference * global_reference option) * obj_typ) list
+  ((global_reference * cs_pattern) * obj_typ) list