* Major code cleanup.

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

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index 5c42f9e76c9efeb0af3dd3c6fbe87bd6e1afc24a..64b7f857cce087cc7f5925654939c2a613768434 100644 (file)
--- a/helm/ocaml/cic/cic.ml
+++ b/helm/ocaml/cic/cic.ml
@@ -93,57 +93,41 @@ and coInductiveFun =
  string * term * term                         (* name, type, body *)
 
 and annterm =
-   ARel of id * annotation option ref *
-    int * string option                             (* DeBrujin index, binder *)
- | AVar of id * annotation option ref *             
-    UriManager.uri                                  (* uri *)
- | AMeta of id * annotation option ref * int        (* numeric id *)
- | ASort of id * annotation option ref * sort       (* sort *)
- | AImplicit of id * annotation option ref          (* *)
- | ACast of id * annotation option ref *
-    annterm * annterm                               (* value, type *)
- | AProd of id * annotation option ref *
-    name * annterm * annterm                        (* binder, source, target *)
- | ALambda of id * annotation option ref *
-    name * annterm * annterm                        (* binder, source, target *)
- | ALetIn of id * annotation option ref *
-    name * annterm * annterm                        (* binder, term, target *)
- | AAppl of id * annotation option ref *
-    annterm list                                    (* arguments *)
- | AConst of id * annotation option ref *
-    UriManager.uri * int                            (* uri, number of cookings*)
- | AAbst of id * annotation option ref *
-    UriManager.uri                                  (* uri *)
- | AMutInd of id * annotation option ref *
-    UriManager.uri * int * int                      (* uri, cookingsno, typeno*)
- | AMutConstruct of id * annotation option ref *
-    UriManager.uri * int *                          (* uri, cookingsno, *)
+   ARel of id * int * string                        (* DeBrujin index, binder *)
+ | AVar of id * UriManager.uri                      (* uri *)
+ | AMeta of id * int                                (* numeric id *)
+ | ASort of id * sort                               (* sort *)
+ | AImplicit of id                                  (* *)
+ | 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 *)
+ | 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*)
+ | AMutConstruct of id * UriManager.uri * int *     (* uri, cookingsno, *)
     int * int                                       (*  typeno, consno  *)
  (*CSC: serve cookingsno?*)
- | AMutCase of id * annotation option ref *
-    UriManager.uri * int *                          (* ind. uri, cookingsno  *)
+ | AMutCase of id * UriManager.uri * int *          (* ind. uri, cookingsno  *)
     int *                                           (*  ind. typeno,         *)
     annterm * annterm *                             (*  outtype, ind. term   *)
     annterm list                                    (*  patterns             *)
- | AFix of id * annotation option ref *
-    int * anninductiveFun list                      (* funno, functions *)
- | ACoFix of id * annotation option ref *
-    int * anncoInductiveFun list                    (* funno, functions *)
+ | AFix of id * int * anninductiveFun list          (* funno, functions *)
+ | ACoFix of id * int * anncoInductiveFun list      (* funno, functions *)
 and annobj =
-   ADefinition of id * annotation option ref *
-    string *                                        (* id,           *)
+   ADefinition of id * string *                     (* id,           *)
     annterm * annterm *                             (*  value, type, *)
     (int * UriManager.uri list) list exactness      (*  parameters   *)
- | AAxiom of id * annotation option ref *
-    string * annterm *                              (* id, type    *)
+ | AAxiom of id * string * annterm *                (* id, type    *)
     (int * UriManager.uri list) list                (*  parameters *)
- | AVariable of id * annotation option ref *
+ | AVariable of id *
     string * annterm option * annterm               (* name, body, type *)
- | ACurrentProof of id * annotation option ref *
+ | ACurrentProof of id *
     string * (int * annterm) list *                 (*  name, conjectures, *)
     annterm * annterm                               (*  value, type        *)
  | AInductiveDefinition of id *
-    annotation option ref * anninductiveType list * (* inductive types ,      *)
+    anninductiveType list *                         (* inductive types ,      *)
     (int * UriManager.uri list) list * int          (*  parameters,n ind. pars*)
 and anninductiveType = 
  string * bool * annterm *                    (* typename, inductive, arity *)