From 0d6f5efcf10a888bfccc769f2c58d998c411da47 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 27 Sep 2009 20:33:46 +0000 Subject: [PATCH 1/1] fixpoint have attributes for pragma (i.e. they can be marked as projections) --- .../software/components/ng_disambiguation/nCicDisambiguate.ml | 2 +- helm/software/components/ng_kernel/nCic.ml | 2 +- helm/software/components/ng_kernel/oCic2NCic.ml | 4 ++-- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index 6bf1c05ba..4ea6e5ac3 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -484,7 +484,7 @@ let interpretate_obj ([],ncic_name_of_ident name, decr_idx, cic_type, cic_body)) defs in - let attrs = `Provided, new_flavour_of_flavour flavour in + let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in NCic.Fixpoint (inductive,inductiveFuns,attrs) | bo -> let bo = diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml index c531d1c2b..f39cf868e 100644 --- a/helm/software/components/ng_kernel/nCic.ml +++ b/helm/software/components/ng_kernel/nCic.ml @@ -98,7 +98,7 @@ type ind_pragma = (* pragmatic of the object *) type generated = [ `Generated | `Provided ] type c_attr = generated * def_flavour * def_pragma -type f_attr = generated * def_flavour +type f_attr = generated * def_flavour * def_pragma type i_attr = generated * ind_pragma (* invariant: metasenv and substitution have disjoint domains *) diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index 7bfb6c39c..1487881c1 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -546,7 +546,7 @@ and height_of_term ?(h=ref 0) t = in let obj = nuri_of_ouri buri,0,[],[], - NCic.Fixpoint (false, fl, (`Generated, `Definition)) + NCic.Fixpoint (false, fl, (`Generated, `Definition, `Regular)) in let r = reference_of_ouri buri (Ref.CoFix cofixno) in let obj,r = @@ -607,7 +607,7 @@ and height_of_term ?(h=ref 0) t = in let obj = nuri_of_ouri buri,height,[],[], - NCic.Fixpoint (true, fl, (`Generated, `Definition)) in + NCic.Fixpoint (true, fl, (`Generated, `Definition, `Regular)) in (*prerr_endline ("H(" ^ UriManager.string_of_uri buri ^ ") = " ^ string_of_int * height);*) let r = reference_of_ouri buri (Ref.Fix (fixno,!rno_fixno,height)) in let obj,r = -- 2.39.2