First very partial implementation of LetIn and bodyed Variables

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

diff --git a/helm/interface/cic.ml b/helm/interface/cic.ml
index dd919253163631c6bd170f6727be4f4dab830369..1028f328790f474c0a660bfdc890186252972bb3 100644 (file)
--- a/helm/interface/cic.ml
+++ b/helm/interface/cic.ml
@@ -33,6 +33,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 +52,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 +81,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 +113,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        *)