cic defined (half)

diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml
index 2ff591ffc3052c4ea73e10ae4fe4a1c45c917b83..28e2fbd0593b89c8d0cd9386d20e0d6fed6be95e 100644 (file)
--- 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 =