fixpoint have attributes for pragma (i.e. they can be marked as projections)

[helm.git] / helm / software / components / ng_disambiguation / nCicDisambiguate.ml

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index 6bf1c05ba0226ab739812b82d02cd2f95acad3a4..4ea6e5ac3e4dd3ee47655f62a2ac1ed05254dc8f 100644 (file)
--- 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 =