X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2Fcic.ml;h=a556aadca6b184b213d0f2915bd2143964a10080;hb=b57c31a1593872c181249135bc05ebd9a72f523b;hp=550d4a8f6d306f14dd1caba58b7a183503784a8b;hpb=82466efd82082c6101d1c2c0c217f681b37160e8;p=helm.git

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index 550d4a8f6..a556aadca 100644
--- a/helm/ocaml/cic/cic.ml
+++ b/helm/ocaml/cic/cic.ml
@@ -40,6 +40,8 @@ type id = string  (* the abstract type of the (annotated) node identifiers *)
 type anntarget =
    Object of annobj
  | Term of annterm
+ | Conjecture of annconjecture
+ | Hypothesis of annhypothesis
 
 (* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *)
 and sort =
@@ -93,9 +95,13 @@ and inductiveFun =
 and coInductiveFun =
  string * term * term                         (* name, type, body *)
 
-and metasenv = (int * context * term) list (* a metasenv is a list of declarations of metas *)
+(* a metasenv is a list of declarations of metas *)
+and conjecture = int * context * term
+and metasenv = conjecture list
 
-and annmetasenv = (int * anncontext * annterm) list (* a metasenv is a list of declarations of metas *)
+(* a metasenv is a list of declarations of metas *)
+and annconjecture = id * int * anncontext * annterm
+and annmetasenv = annconjecture list
 
 and annterm =
    ARel of id * int * string                        (* DeBrujin index, binder *)
@@ -150,14 +156,20 @@ and 'a exactness =
    Possible of 'a                            (* an approximation to something *)
  | Actual of 'a                              (* something *)
 
-and context_entry =                    (* Contexts are lists of context_entry *)
+and context_entry =                            (* A declaration or definition *)
    Decl of term
  | Def of term
 
-and context = ((name * context_entry) option) list
+and hypothesis =
+ (name * context_entry) option               (* None means no more accessible *)
 
-and anncontext_entry =                 (* Contexts are lists of context_entry *)
+and context = hypothesis list
+
+and anncontext_entry =                         (* A declaration or definition *)
    ADecl of annterm
  | ADef of annterm
 
-and anncontext = ((name * anncontext_entry) option) list;;
+and annhypothesis =
+ id * (name * anncontext_entry) option       (* None means no more accessible *)
+
+and anncontext = annhypothesis list;;