in the new kernel you can type Type[i] to mean Type_i, and Type is interpreted as

[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 f0a3fa0eb7386ba9747243c4050d718ed2ffeea7..5ded5b886370c7c9230e9bfd6323e7be8522db3c 100644 (file)
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -316,7 +316,7 @@ let interpretate_term_and_interpretate_term_option
     | CicNotationPt.Ident (name, subst) ->
        assert (subst = None);
        (try
-         NCic.Rel (find_in_context name context)
+             NCic.Rel (find_in_context name context)
        with Not_found -> 
          try NCic.Const (List.assoc name obj_context)
          with Not_found ->
@@ -342,11 +342,13 @@ let interpretate_term_and_interpretate_term_option
     | CicNotationPt.Sort `Set -> NCic.Sort (NCic.Type
        [false,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/Type.univ"])
+       [false,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")])
+    | CicNotationPt.Sort (`NCProp s) -> NCic.Sort (NCic.Type
+       [false,NUri.uri_of_string ("cic:/matita/pts/CProp" ^ s ^ ".univ")])
     | CicNotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type
-       [false,NUri.uri_of_string "cic:/matita/pts/CProp.univ"])
+       [false,NUri.uri_of_string "cic:/matita/pts/CProp0.univ"])
     | CicNotationPt.Symbol (symbol, instance) ->
         Disambiguate.resolve ~env ~mk_choice 
          (Symbol (symbol, instance)) (`Args [])
@@ -647,6 +649,7 @@ let disambiguate_obj
    in
     List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
 ;;
+(*
 let _ = 
 let mk_type n = 
   if n = 0 then
@@ -685,4 +688,5 @@ in
          NCicEnvironment.add_constraint false (mk_type 3) (mk_cprop 3);
 
 ;;
+*)