From: Enrico Tassi <enrico.tassi@inria.fr>
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 =