]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic/cic.ml
Abst removed from the DTD.
[helm.git] / helm / ocaml / cic / cic.ml
index a556aadca6b184b213d0f2915bd2143964a10080..fd3e191a81a306461e8343bd764fb9639de81650 100644 (file)
@@ -64,7 +64,6 @@ 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*)
  | MutConstruct of UriManager.uri * int *           (* uri, cookingsno, *)
     int * int                                       (*  typeno, consno  *)
@@ -116,7 +115,6 @@ 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*)
  | AMutConstruct of id * UriManager.uri * int *     (* uri, cookingsno, *)
     int * int                                       (*  typeno, consno  *)