From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 5 Feb 2008 17:45:38 +0000 (+0000)
Subject: cic defined (half)
X-Git-Tag: make_still_working~5627
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a2a94eaf6a7ceb1c829973b97520c917cd1da270;p=helm.git

cic defined (half)
---

diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml
index 2ff591ffc..28e2fbd05 100644
--- a/helm/software/components/ng_kernel/nCic.ml
+++ b/helm/software/components/ng_kernel/nCic.ml
@@ -43,15 +43,17 @@ and term =
  | Prod     of name * term * term                     (* binder, source, target          *)
  | Lambda   of name * term * term                     (* binder, source, target          *)
  | LetIn    of name * term * term * term              (* binder, type, term, body        *)
- | Const    of NUriManager.reference                  (* reference contains indtypeno/constrno *)
+(* Cast \def degenerate LetIn *)
+ | Const    of NReference.reference                  (* reference contains indtypeno/constrno *)
  | Sort     of sort                                   (* sort                            *)
  | Implicit of implicit_annotation                    (* ... *)
- | MutCase  of NUriManager.reference *                (* ind. reference,             *)
+ | Match    of NReference.reference *                (* ind. reference,             *)
     term * term *                                     (*  outtype, ind. term   *)
     term list                                         (*  patterns             *)
 
 and obj =
  | Constant of term option * term
+ | FixpointDefinition  of ...
  | InductiveDefinition of inductiveType list    (* inductive types,         *)
 
 and inductiveType =