added annotations to Cic.Implicit

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

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index 46126ff319236800f1a800ad255e2338a9bc24ef..55a338b3f3b54b7644894e6eceb194c40a258de0 100644 (file)
--- a/helm/ocaml/cic/cic.ml
+++ b/helm/ocaml/cic/cic.ml
@@ -39,6 +39,8 @@
 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
@@ -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 *)
@@ -123,7 +125,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 *)