From a2a94eaf6a7ceb1c829973b97520c917cd1da270 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 5 Feb 2008 17:45:38 +0000 Subject: [PATCH] cic defined (half) --- helm/software/components/ng_kernel/nCic.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) 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 = -- 2.39.2