Conjectures and Hypotheses inside every conjecture and in the sequents now

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

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index 550d4a8f6d306f14dd1caba58b7a183503784a8b..a556aadca6b184b213d0f2915bd2143964a10080 100644 (file)
--- 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;;