From f67ba2fcc539161947b5cdde1b9516a3817115d6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 13 Feb 2008 13:17:38 +0000 Subject: [PATCH] factorized common components of objects --- helm/software/components/ng_kernel/nCic.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml index 43f6c86d9..19a8a227b 100644 --- a/helm/software/components/ng_kernel/nCic.ml +++ b/helm/software/components/ng_kernel/nCic.ml @@ -86,7 +86,7 @@ type def_pragma = (* pragmatic of the object *) | `Projection (* record projection *) | `InversionPrinciple (* inversion principle *) | `Variant - | `Local ] (* Local = hidden technicality *) + | `Local ] (* Local = hidden technicality *) type ind_pragma = (* pragmatic of the object *) [ `Record of (string * bool * int) list ] @@ -100,9 +100,10 @@ type f_attr = generated * def_flavour type i_attr = generated * ind_pragma (* invariant: metasenv and substitution have disjoint domains *) -type obj = - | Constant of NUri.uri * metasenv * substitution * relevance * string * term option * term * c_attr - | Fixpoint of NUri.uri * metasenv * substitution * bool * inductiveFun list * f_attr - | Inductive of NUri.uri * metasenv * substitution * bool * int * inductiveType list * i_attr - (* uri, menv, subst, (co)inductive, leftno, types *) +type obj_kind = + | Constant of relevance * string * term option * term * c_attr + | Fixpoint of bool * inductiveFun list * f_attr + | Inductive of bool * int * inductiveType list * i_attr + (* (co)inductive, leftno, types *) +type obj = NUri.uri * int * metasenv * substitution * obj_kind -- 2.39.2