...

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

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index a556aadca6b184b213d0f2915bd2143964a10080..2429dcfeddb51b4bc2ec24fb6aa6e52143a0d03e 100644 (file)
--- a/helm/ocaml/cic/cic.ml
+++ b/helm/ocaml/cic/cic.ml
@@ -64,10 +64,11 @@ and term =
  | LetIn of name * term * term                      (* binder, term, target *)
  | Appl of term list                                (* arguments *)
  | Const of UriManager.uri * int                    (* uri, number of cookings*)
- | Abst of UriManager.uri                           (* uri *)
  | MutInd of UriManager.uri * int * int             (* uri, cookingsno, typeno*)
+                                                    (* typeno is 0 based *)
  | MutConstruct of UriManager.uri * int *           (* uri, cookingsno, *)
     int * int                                       (*  typeno, consno  *)
+                                                    (* consno is 1 based *)
  (*CSC: serve cookingsno?*)
  | MutCase of UriManager.uri * int *                (* ind. uri, cookingsno, *)
     int *                                           (*  ind. typeno,         *)
@@ -116,10 +117,11 @@ and annterm =
  | ALetIn of id * name * annterm * annterm          (* binder, term, target *)
  | AAppl of id * annterm list                       (* arguments *)
  | AConst of id * UriManager.uri * int              (* uri, number of cookings*)
- | AAbst of id * UriManager.uri                     (* uri *)
  | AMutInd of id * UriManager.uri * int * int       (* uri, cookingsno, typeno*)
+                                                    (* typeno is 0 based *)
  | AMutConstruct of id * UriManager.uri * int *     (* uri, cookingsno, *)
     int * int                                       (*  typeno, consno  *)
+                                                    (* consno is 1 based *)
  (*CSC: serve cookingsno?*)
  | AMutCase of id * UriManager.uri * int *          (* ind. uri, cookingsno  *)
     int *                                           (*  ind. typeno,         *)