X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2Fcic.ml;h=9a4f4b0dedde0fefe8ad8db133207c88804a7af0;hb=HEAD;hp=1becd44428bd3b4f9139c01280e0d47ef48de26e;hpb=1aa36efd14e9d62adf8232f37bdf55101c70ba43;p=helm.git

diff --git a/helm/software/components/cic/cic.ml b/helm/software/components/cic/cic.ml
index 1becd4442..9a4f4b0de 100644
--- a/helm/software/components/cic/cic.ml
+++ b/helm/software/components/cic/cic.ml
@@ -49,7 +49,7 @@ type sort =
    Prop
  | Set
  | Type of CicUniv.universe
- | CProp
+ | CProp of CicUniv.universe
 
 type name =
  | Name of string
@@ -57,21 +57,24 @@ type name =
 
 type object_flavour =
   [ `Definition
+  | `MutualDefinition
   | `Fact
   | `Lemma
   | `Remark
   | `Theorem
   | `Variant
+  | `Axiom
   ]
 
 type object_class =
-  [ `Coercion
-  | `Elim of sort   (** elimination principle; if sort is Type, the universe is
+  [ `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 =
@@ -91,7 +94,7 @@ type term =
  | Cast of term * term                              (* value, type *)
  | Prod of name * term * term                       (* binder, source, target *)
  | Lambda of name * term * term                     (* binder, source, target *)
- | LetIn of name * term * term                      (* binder, term, target *)
+ | LetIn of name * term * term * term               (* binder, term, type, target *)
  | Appl of term list                                (* arguments *)
  | Const of UriManager.uri *                        (* uri,                   *)
      term explicit_named_substitution               (*  explicit named subst. *)
@@ -155,7 +158,7 @@ and annterm =
  | ACast of id * annterm * annterm                  (* value, type *)
  | AProd of id * name * annterm * annterm           (* binder, source, target *)
  | ALambda of id * name * annterm * annterm         (* binder, source, target *)
- | ALetIn of id * name * annterm * annterm          (* binder, term, target *)
+ | ALetIn of id * name * annterm * annterm *  annterm (* binder, term, type, target *)
  | AAppl of id * annterm list                       (* arguments *)
  | AConst of id * UriManager.uri *                  (* uri,                   *)
     annterm explicit_named_substitution             (*  explicit named subst. *)
@@ -201,7 +204,7 @@ and annotation =
 
 and context_entry =                            (* A declaration or definition *)
    Decl of term
- | Def of term * term option                   (* body, type (if known) *)
+ | Def of term * term                          (* body, type *)
 
 and hypothesis =
  (name * context_entry) option               (* None means no more accessible *)
@@ -210,7 +213,7 @@ and context = hypothesis list
 
 and anncontext_entry =                         (* A declaration or definition *)
    ADecl of annterm
- | ADef of annterm
+ | ADef of annterm * annterm
 
 and annhypothesis =
  id * (name * anncontext_entry) option       (* None means no more accessible *)