new snapshot

[helm.git] / components / cic / cic.ml

diff --git a/components/cic/cic.ml b/components/cic/cic.ml
index 64825e505dbc717585e0b444cd19e97d1c3762a9..1b02df3f1a12c7367a64a64cdc49fad3f7d1d9c0 100644 (file)
--- a/components/cic/cic.ml
+++ b/components/cic/cic.ml
@@ -57,21 +57,25 @@ type name =
 
 type object_flavour =
   [ `Definition
+  | `MutualDefinition
   | `Fact
   | `Lemma
   | `Remark
   | `Theorem
   | `Variant
+  | `Axiom
   ]
 
 type object_class =
-  [ `Coercion
+  [ `Coercion of int
   | `Elim of sort   (** elimination principle; if sort is Type, the universe is
                       * not relevant *)
-  | `Record of (string * bool) list (** 
+  | `Record of (string * bool * int) list (** 
                         inductive type that encodes a record; the arguments are
-                        the record fields names and if they are coercions *)
+                        the record fields names and if they are coercions and
+                        then the coercion arity *)
   | `Projection     (** record projection *)
+  | `InversionPrinciple (** inversion principle *)
   ]
 
 type attribute =
@@ -234,7 +238,7 @@ module CicHash =
   (struct
     type t = term
     let equal = (==)
-    let hash = Hashtbl.hash
+    let hash = Hashtbl.hash_param 100 1000 
    end)
 ;;