X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Finterface%2Fcic.ml;h=8c08b0075dec425113df9f2bacae31a67b12f6c1;hb=4faf0e37e7019de16dd6862bb34d84f799a2a230;hp=dd919253163631c6bd170f6727be4f4dab830369;hpb=c01d2aaea05f7385bee46addd900cd0397756389;p=helm.git

diff --git a/helm/interface/cic.ml b/helm/interface/cic.ml
index dd9192531..8c08b0075 100644
--- a/helm/interface/cic.ml
+++ b/helm/interface/cic.ml
@@ -1,3 +1,28 @@
+(* Copyright (C) 2000, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
 (******************************************************************************)
 (*                                                                            *)
 (*                               PROJECT HELM                                 *)
@@ -33,6 +58,7 @@ and term =
  | Cast of term * term                              (* value, type *)
  | Prod of name * term * term                       (* binder, source, target *)
  | Lambda of name * term * term                     (* binder, source, target *)
+ | 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 *)
@@ -51,7 +77,7 @@ and obj =
     (int * UriManager.uri list) list              (*  parameters              *)
  | Axiom of string * term *
     (int * UriManager.uri list) list              (* id, type, parameters     *)
- | Variable of string * term                      (* name, type               *)
+ | Variable of string * term option * term        (* name, body, type         *)
  | CurrentProof of string * (int * term) list *   (* name, conjectures,       *)
     term * term                                   (*  value, type             *)
  | InductiveDefinition of inductiveType list *    (* inductive types,         *)
@@ -80,6 +106,8 @@ and annterm =
     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 *
@@ -110,7 +138,7 @@ and annobj =
     string * annterm *                              (* id, type    *)
     (int * UriManager.uri list) list                (*  parameters *)
  | AVariable of id * annotation option ref *
-    string * annterm                                (* name, type *)
+    string * annterm option * annterm               (* name, body, type *)
  | ACurrentProof of id * annotation option ref *
     string * (int * annterm) list *                 (*  name, conjectures, *)
     annterm * annterm                               (*  value, type        *)