X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2Fcic.ml;h=7dc86114d7e72d82eff94fbde167a9576deaeca2;hb=0c6a5aadb1a7746681a8e26fc0b009f847c10557;hp=46126ff319236800f1a800ad255e2338a9bc24ef;hpb=0fd7e4864dbcd0f3e04ed71bb654ff616b7e4a79;p=helm.git

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index 46126ff31..7dc86114d 100644
--- a/helm/ocaml/cic/cic.ml
+++ b/helm/ocaml/cic/cic.ml
@@ -23,22 +23,24 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
-(*                                 29/11/2000                                 *)
-(*                                                                            *)
-(* This module defines the internal representation of the objects (variables, *)
-(* blocks of (co)inductive definitions and constants) and the terms of cic    *)
-(*                                                                            *)
-(******************************************************************************)
+(*****************************************************************************)
+(*                                                                           *)
+(*                               PROJECT HELM                                *)
+(*                                                                           *)
+(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>              *)
+(*                                 29/11/2000                                *)
+(*                                                                           *)
+(* This module defines the internal representation of the objects (variables,*)
+(* blocks of (co)inductive definitions and constants) and the terms of cic   *)
+(*                                                                           *)
+(*****************************************************************************)
 
 (* STUFF TO MANAGE IDENTIFIERS *)
 type id = string  (* the abstract type of the (annotated) node identifiers *)
 type 'term explicit_named_substitution = (UriManager.uri * 'term) list
 
+type implicit_annotation = [ `Closed | `Type ]
+
 type anntarget =
    Object of annobj         (* if annobj is a Constant, this is its type *)
  | ConstantBody of annobj
@@ -50,7 +52,7 @@ type anntarget =
 and sort =
    Prop
  | Set
- | Type
+ | Type of CicUniv.universe
  | CProp
 and name =
    Name of string
@@ -62,7 +64,7 @@ and term =
  | Meta of int * (term option) list                 (* numeric id,    *)
                                                     (*  local context *)
  | Sort of sort                                     (* sort *)
- | Implicit                                         (* *)
+ | Implicit of implicit_annotation option           (* *)
  | Cast of term * term                              (* value, type *)
  | Prod of name * term * term                       (* binder, source, target *)
  | Lambda of name * term * term                     (* binder, source, target *)
@@ -108,6 +110,9 @@ and coInductiveFun =
 (* depend on new ones.                                           *)
 and conjecture = int * context * term
 and metasenv = conjecture list
+and substitution = (int * (context * term)) list
+
+
 
 (* a metasenv is a list of declarations of metas in declarations *)
 (* order (i.e. [oldest ; ... ; newest]). Older variables can not *)
@@ -123,7 +128,7 @@ and annterm =
  | AMeta of id * int * (annterm option) list        (* numeric id,    *)
                                                     (*  local context *)
  | ASort of id * sort                               (* sort *)
- | AImplicit of id                                  (* *)
+ | AImplicit of id * implicit_annotation option     (* *)
  | 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 *)