X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2Fcic.ml;h=64825e505dbc717585e0b444cd19e97d1c3762a9;hb=5104e38ee747fd1052ce21f3f9f2ecc778d590ba;hp=23bb7661b0bb4d8b96340c032f73e67970760656;hpb=f47b833df94d134090a65653077744290438a875;p=helm.git

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index 23bb7661b..64825e505 100644
--- a/helm/ocaml/cic/cic.ml
+++ b/helm/ocaml/cic/cic.ml
@@ -35,6 +35,8 @@
 (*                                                                           *)
 (*****************************************************************************)
 
+(* $Id$ *)
+
 (* STUFF TO MANAGE IDENTIFIERS *)
 type id = string  (* the abstract type of the (annotated) node identifiers *)
 type 'term explicit_named_substitution = (UriManager.uri * 'term) list
@@ -53,16 +55,28 @@ type name =
  | Name of string
  | Anonymous
 
+type object_flavour =
+  [ `Definition
+  | `Fact
+  | `Lemma
+  | `Remark
+  | `Theorem
+  | `Variant
+  ]
+
 type object_class =
   [ `Coercion
   | `Elim of sort   (** elimination principle; if sort is Type, the universe is
                       * not relevant *)
-  | `Record         (** inductive type that encodes a record *)
+  | `Record of (string * bool) list (** 
+                        inductive type that encodes a record; the arguments are
+                        the record fields names and if they are coercions *)
   | `Projection     (** record projection *)
   ]
 
 type attribute =
   [ `Class of object_class
+  | `Flavour of object_flavour 
   | `Generated
   ]
 
@@ -100,7 +114,7 @@ and obj =
     UriManager.uri list * attribute list          (*  parameters              *)
  | Variable of string * term option * term *      (* name, body, type         *)
     UriManager.uri list * attribute list          (* parameters               *)
- | CurrentProof of string * metasenv * term *     (* name, conjectures, value,*)
+ | CurrentProof of string * metasenv * term *     (* name, conjectures, body, *)
     term * UriManager.uri list * attribute list   (*  type, parameters        *)
  | InductiveDefinition of inductiveType list *    (* inductive types,         *)
     UriManager.uri list * int * attribute list    (*  params, left params no  *)
@@ -168,7 +182,7 @@ and annobj =
     UriManager.uri list * attribute list            (*  parameters      *)
  | ACurrentProof of id * id *
     string * annmetasenv *                          (*  name, conjectures,    *)
-    annterm * annterm * UriManager.uri list *       (*  value,type,parameters *)
+    annterm * annterm * UriManager.uri list *       (*  body,type,parameters  *)
     attribute list
  | AInductiveDefinition of id *
     anninductiveType list *                         (* inductive types ,      *)
@@ -204,6 +218,10 @@ and annhypothesis =
 and anncontext = annhypothesis list
 ;;
 
+type lazy_term =
+ context -> metasenv -> CicUniv.universe_graph ->
+  term * metasenv * CicUniv.universe_graph
+
 type anntarget =
    Object of annobj         (* if annobj is a Constant, this is its type *)
  | ConstantBody of annobj
@@ -211,3 +229,12 @@ type anntarget =
  | Conjecture of annconjecture
  | Hypothesis of annhypothesis
 
+module CicHash =
+ Hashtbl.Make
+  (struct
+    type t = term
+    let equal = (==)
+    let hash = Hashtbl.hash
+   end)
+;;
+