ugly coerc db print

[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 4bfeab669066ad762d7a260515c8a5426ab16a69..4ea6e5ac3e4dd3ee47655f62a2ac1ed05254dc8f 100644 (file)
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -64,7 +64,7 @@ let refine_term
 ;;
 
 let refine_obj 
-  ~rdb metasenv subst context _uri 
+  ~rdb metasenv subst _context _uri 
   ~use_coercions obj _ _ugraph ~localization_tbl 
 =
   assert (metasenv=[]);
@@ -72,7 +72,6 @@ let refine_obj
   let localise t = 
     try NCicUntrusted.NCicHash.find localization_tbl t
     with Not_found -> 
-      prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
       (*assert false*)HExtlib.dummy_floc
   in
   try
@@ -322,7 +321,7 @@ let interpretate_term_and_interpretate_term_option
        with Not_found -> 
          try NCic.Const (List.assoc name obj_context)
          with Not_found ->
-           Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
+            Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
     | CicNotationPt.Uri (uri, subst) ->
        assert (subst = None);
        (try
@@ -344,15 +343,15 @@ let interpretate_term_and_interpretate_term_option
          NCic.Meta (index, (0, NCic.Ctx cic_subst))
     | CicNotationPt.Sort `Prop -> NCic.Sort NCic.Prop
     | CicNotationPt.Sort `Set -> NCic.Sort (NCic.Type
-       [false,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
+       [`Type,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
     | CicNotationPt.Sort (`Type _u) -> NCic.Sort (NCic.Type
-       [false,NUri.uri_of_string "cic:/matita/pts/Type0.univ"])
+       [`Type,NUri.uri_of_string "cic:/matita/pts/Type0.univ"])
     | CicNotationPt.Sort (`NType s) -> NCic.Sort (NCic.Type
-       [false,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
+       [`Type,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
     | CicNotationPt.Sort (`NCProp s) -> NCic.Sort (NCic.Type
-       [false,NUri.uri_of_string ("cic:/matita/pts/CProp" ^ s ^ ".univ")])
+       [`CProp,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
     | CicNotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type
-       [false,NUri.uri_of_string "cic:/matita/pts/CProp0.univ"])
+       [`CProp,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
     | CicNotationPt.Symbol (symbol, instance) ->
         Disambiguate.resolve ~env ~mk_choice 
          (Symbol (symbol, instance)) (`Args [])
@@ -485,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 =