rewritten instantiate code

[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..ff74d233a7573c63233a57fde2b0ce38e2e4e35b 100644 (file)
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -331,6 +331,7 @@ let interpretate_term_and_interpretate_term_option
     | CicNotationPt.NRef nref -> NCic.Const nref
     | CicNotationPt.Implicit `Vector -> NCic.Implicit `Vector
     | CicNotationPt.Implicit `JustOne -> NCic.Implicit `Term
+    | CicNotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)
     | CicNotationPt.UserInput -> NCic.Implicit `Hole
     | CicNotationPt.Num (num, i) -> 
         Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num)
@@ -484,7 +485,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 =