From: Enrico Tassi Date: Sun, 27 Sep 2009 20:33:46 +0000 (+0000) Subject: fixpoint have attributes for pragma (i.e. they can be marked as projections) X-Git-Tag: make_still_working~3432 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0d6f5efcf10a888bfccc769f2c58d998c411da47;p=helm.git fixpoint have attributes for pragma (i.e. they can be marked as projections) --- 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 =