- added support for contexts (terms with holes)

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

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index c997d99ca3d3a866fbed691f1929803f46149b8c..4f705168860d66e4df77fc2c2d23eb18d7d58915 100644 (file)
--- a/helm/ocaml/cic/cic.ml
+++ b/helm/ocaml/cic/cic.ml
@@ -39,7 +39,7 @@
 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 implicit_annotation = [ `Closed | `Type | `Hole ]
 
 type anntarget =
    Object of annobj         (* if annobj is a Constant, this is its type *)
@@ -58,7 +58,7 @@ and name =
    Name of string
  | Anonymous
 and term =
-   Rel of int                                       (* DeBrujin index *)
+   Rel of int                                       (* DeBrujin index, 1 based*)
  | Var of UriManager.uri *                          (* uri,                   *)
      term explicit_named_substitution               (*  explicit named subst. *)
  | Meta of int * (term option) list                 (* numeric id,    *)
@@ -94,7 +94,7 @@ and obj =
  | CurrentProof of string * metasenv *            (* name, conjectures,       *)
     term * term * UriManager.uri list             (*  value, type, parameters *)
  | InductiveDefinition of inductiveType list *    (* inductive types,         *)
-    UriManager.uri list * int                     (*  parameters, n ind. pars *)
+    UriManager.uri list * int                     (*  params, left params no  *)
 and inductiveType = 
  string * bool * term *                       (* typename, inductive, arity *)
   constructor list                            (*  constructors              *)