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

Type[0]. The same holds for CProp.

tests/ng_pts.ma defines some sorts, you may want to include it

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index 45fa23a0d01d3bc10329801ffccbb7b313d1c5fc..a835e074f40ff48853d9e957de2b9d5d41d13e21 100644 (file)
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/components/acic_content/cicNotationPp.ml
@@ -154,6 +154,7 @@ let rec pp_term ?(pp_parens = true) t =
     | Ast.Sort (`Type _) -> "Type"
     | Ast.Sort (`CProp _)-> "CProp"
     | Ast.Sort (`NType s)-> "Type[" ^ s ^ "]"
+    | Ast.Sort (`NCProp s)-> "CProp[" ^ s ^ "]"
     | Ast.Symbol (name, _) -> "'" ^ name
 
     | Ast.UserInput -> ""

diff --git a/helm/software/components/acic_content/cicNotationPt.ml b/helm/software/components/acic_content/cicNotationPt.ml
index 3ffa9525808119fcd64a423bb1251feab46ea294..46381e4bc505ea6608fc4548af9cf8aec88f1863 100644 (file)
--- a/helm/software/components/acic_content/cicNotationPt.ml
+++ b/helm/software/components/acic_content/cicNotationPt.ml
@@ -29,7 +29,8 @@
 
 type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ]
 type induction_kind = [ `Inductive | `CoInductive ]
-type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe | `NType of string]
+type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of
+CicUniv.universe | `NType of string |`NCProp of string]
 type fold_kind = [ `Left | `Right ]
 
 type location = Stdpp.location

diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml
index fb890915298b5bb70846c1cc01e1337e56c3ba5f..c02c5892d65aa62583d0dc0a1bd93c6a8184ff22 100644 (file)
--- a/helm/software/components/acic_content/termAcicContent.ml
+++ b/helm/software/components/acic_content/termAcicContent.ml
@@ -126,7 +126,7 @@ let ast_of_acic0 ~output_type term_info acic k =
         let binder_kind =
           match sort_of_id id with
           | `Set | `Type _ | `NType _ -> `Pi
-          | `Prop | `CProp _ -> `Forall
+          | `Prop | `CProp _ | `NCProp _ -> `Forall
         in
         idref id (Ast.Binder (binder_kind,
           (CicNotationUtil.name_of_cic_name n, Some (k s)), k t))

diff --git a/helm/software/components/binaries/extractor/.depend b/helm/software/components/binaries/extractor/.depend
index 0c39328ae147e8ab714b2d3a7b1582a011b2b1d6..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644 (file)
--- a/helm/software/components/binaries/extractor/.depend
+++ b/helm/software/components/binaries/extractor/.depend
@@ -1,4 +0,0 @@
-extractor.cmo: 
-extractor.cmx: 
-extractor_manager.cmo: 
-extractor_manager.cmx: 

diff --git a/helm/software/components/binaries/extractor/.depend.opt b/helm/software/components/binaries/extractor/.depend.opt
index 0c39328ae147e8ab714b2d3a7b1582a011b2b1d6..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644 (file)
--- a/helm/software/components/binaries/extractor/.depend.opt
+++ b/helm/software/components/binaries/extractor/.depend.opt
@@ -1,4 +0,0 @@
-extractor.cmo: 
-extractor.cmx: 
-extractor_manager.cmo: 
-extractor_manager.cmx: 

diff --git a/helm/software/components/binaries/table_creator/.depend b/helm/software/components/binaries/table_creator/.depend
index 33147b94948d28fc9c7132773964d2547472c2ba..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644 (file)
--- a/helm/software/components/binaries/table_creator/.depend
+++ b/helm/software/components/binaries/table_creator/.depend
@@ -1,2 +0,0 @@
-table_creator.cmo: 
-table_creator.cmx: 

diff --git a/helm/software/components/binaries/table_creator/.depend.opt b/helm/software/components/binaries/table_creator/.depend.opt
index 33147b94948d28fc9c7132773964d2547472c2ba..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644 (file)
--- a/helm/software/components/binaries/table_creator/.depend.opt
+++ b/helm/software/components/binaries/table_creator/.depend.opt
@@ -1,2 +0,0 @@
-table_creator.cmo: 
-table_creator.cmx: 

diff --git a/helm/software/components/binaries/transcript/.depend b/helm/software/components/binaries/transcript/.depend
index 87d1ed25c2745435771cee189c10da4a99854448..bb6f22a64b02f88c3881f2c3f490d7f81b186897 100644 (file)
--- a/helm/software/components/binaries/transcript/.depend
+++ b/helm/software/components/binaries/transcript/.depend
@@ -1,11 +1,6 @@
 gallina8Parser.cmi: types.cmo 
 grafiteParser.cmi: types.cmo 
 grafite.cmi: types.cmo 
-engine.cmi: 
-types.cmo: 
-types.cmx: 
-options.cmo: 
-options.cmx: 
 gallina8Parser.cmo: types.cmo options.cmo gallina8Parser.cmi 
 gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi 
 gallina8Lexer.cmo: options.cmo gallina8Parser.cmi 

diff --git a/helm/software/components/binaries/transcript/.depend.opt b/helm/software/components/binaries/transcript/.depend.opt
index f17459162ce81c0ad9c5352cca5e9d99f43cb81c..efadc681eee16cb3cd170845fdd1c7549fbb89b0 100644 (file)
--- a/helm/software/components/binaries/transcript/.depend.opt
+++ b/helm/software/components/binaries/transcript/.depend.opt
@@ -1,11 +1,6 @@
 gallina8Parser.cmi: types.cmx 
 grafiteParser.cmi: types.cmx 
 grafite.cmi: types.cmx 
-engine.cmi: 
-types.cmo: 
-types.cmx: 
-options.cmo: 
-options.cmx: 
 gallina8Parser.cmo: types.cmx options.cmx gallina8Parser.cmi 
 gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi 
 gallina8Lexer.cmo: options.cmx gallina8Parser.cmi 

diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml
index 9ad05dc926725e75b9ca287ebc4b8e3324ae4a9e..3285dcc15fc53e343ffbe7a5de18d2a6a6ea9de8 100644 (file)
--- a/helm/software/components/cic_acic/cic2acic.ml
+++ b/helm/software/components/cic_acic/cic2acic.ml
@@ -25,13 +25,14 @@
 
 (* $Id$ *)
 
-type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe | `NType of string ]
+type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe | `NType of string | `NCProp of string]
 
 let string_of_sort = function
   | `Prop -> "Prop"
   | `Set -> "Set"
   | `Type u -> "Type:" ^ string_of_int (CicUniv.univno u) ^ ":" ^ UriManager.string_of_uri (CicUniv.univuri u)
   | `NType s -> "Type[" ^ s ^ "]"
+  | `NCProp s -> "CProp[" ^ s ^ "]"
   | `CProp u -> "CProp:" ^ string_of_int (CicUniv.univno u) ^ ":" ^ UriManager.string_of_uri (CicUniv.univuri u)
 
 

diff --git a/helm/software/components/cic_acic/cic2acic.mli b/helm/software/components/cic_acic/cic2acic.mli
index 9182ad618794b21c5fa6b6c86d3ca5d74ab21dba..0bf874e86fd45ae6bab8564d1ea98ed3b271b59e 100644 (file)
--- a/helm/software/components/cic_acic/cic2acic.mli
+++ b/helm/software/components/cic_acic/cic2acic.mli
@@ -31,7 +31,7 @@ type anntypes =
  {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option}
 ;;
 
-type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe | `NType of string ]
+type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe | `NType of string | `NCProp of string]
 
 val string_of_sort: sort_kind -> string
 (*val sort_of_string: string -> sort_kind*)

diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.ml b/helm/software/components/cic_disambiguation/cicDisambiguate.ml
index 3e9124e69bd2398c3eef1a02241d4154d1c607b7..b869536bf495cf5e3046a144be2bb39a1d983cde 100644 (file)
--- a/helm/software/components/cic_disambiguation/cicDisambiguate.ml
+++ b/helm/software/components/cic_disambiguation/cicDisambiguate.ml
@@ -496,6 +496,7 @@ let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri
     | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
     | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
     | CicNotationPt.Sort (`NType _) -> Cic.Sort (Cic.Type (CicUniv.fresh ()))
+    | CicNotationPt.Sort (`NCProp _) -> Cic.Sort (Cic.CProp (CicUniv.fresh ()))
     | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)
     | CicNotationPt.Symbol (symbol, instance) ->
         Disambiguate.resolve ~mk_choice ~env

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 8ddb78781a1f74214bb7ad4cdebc8de8241693fc..14032d4512994e54c2c72fd404848a1ebee7e72b 100644 (file)
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -581,8 +581,9 @@ EXTEND
   sort: [
     [ "Prop" -> `Prop
     | "Set" -> `Set
-    | "Type"; SYMBOL "["; n = NUMBER; SYMBOL "]" -> `NType n 
+    | "Type"; SYMBOL "["; n = NUMBER; SYMBOL "]" -> `NType n
     | "Type" -> `Type (CicUniv.fresh ()) 
+    | "CProp"; SYMBOL "["; n = NUMBER; SYMBOL "]" -> `NCProp n
     | "CProp" -> `CProp (CicUniv.fresh ())
     ]
   ];

diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml
index 85f4a3187ea641290d98c2fd75118e15912fedb0..00f6c978982b5f7904f30a098c2eb699a401cd94 100644 (file)
--- a/helm/software/components/content_pres/termContentPres.ml
+++ b/helm/software/components/content_pres/termContentPres.ml
@@ -94,6 +94,7 @@ let string_of_sort_kind = function
   | `CProp _ -> "CProp"
   | `Type _ -> "Type"
   | `NType s -> "Type[" ^ s ^ "]"
+  | `NCProp s -> "CProp[" ^ s ^ "]"
 
 let map_space f l =
  HExtlib.list_concat

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index a2d1ef655cc09922eb497490d6b7f4f7639c8fcc..c61319233f3f735bf264c4407549f435d8efacb0 100644 (file)
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -171,7 +171,7 @@ type ('term,'lazy_term) macro =
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)
-let magic = 19
+let magic = 20
 
 type ('term,'obj) command =
   | Index of loc * 'term option (* key *) * UriManager.uri (* value *)
@@ -192,6 +192,7 @@ type ('term,'obj) command =
   | Print of loc * string
   | Qed of loc
   | NObj of loc * CicNotationPt.term CicNotationPt.obj
+  | NUnivConstraint of loc * bool * NUri.uri * NUri.uri
   | NQed of loc
 
 type punctuation_tactical =

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 6806713a4e9375a4c20ca4009d666c54d62720ea..70acd56d8fc15730e8a40564c7d6bb201a1a62a1 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -358,6 +358,9 @@ let pp_command ~term_pp ~obj_pp = function
   | Print (_,s) -> "print " ^ s
   | Set (_, name, value) -> Printf.sprintf "set \"%s\" \"%s\"" name value
   | NObj (_,o) -> "not supported"
+  | NUnivConstraint (_) -> "not supported"
+  | NQed (_) -> "not supported"
+  | Pump (_) -> "not supported"
 
 let pp_punctuation_tactical =
   function

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index ccd02981f2f4f5a5516eb861dbca2e1cae29ca99..037a36f38ca164790ba9b5af23f75c88c752d841 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -789,6 +789,9 @@ prerr_endline "CSC: here we should fix the height!!!";
      status, `Old [] (*CSC: TO BE FIXED *)
   | GrafiteAst.Set (loc, name, value) -> status, `Old []
 (*       GrafiteTypes.set_option status name value,[] *)
+  | GrafiteAst.NUnivConstraint (loc,strict,u1,u2) ->
+      NCicEnvironment.add_constraint strict [false,u1] [false,u2];
+      status, `New [u1;u2]
   | GrafiteAst.NObj (loc,obj) ->
      let lexicon_status =
        match status.GrafiteTypes.ng_status with

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 8830a600dbaa315497030e0c61c716ab19b1c5b7..e94507a86bc28a7286be49d1bcad1474752bebd5 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -836,6 +836,7 @@ let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
    | GrafiteAst.Print _
    | GrafiteAst.Qed _
    | GrafiteAst.NQed _
+   | GrafiteAst.NUnivConstraint _
    | GrafiteAst.Set _ as cmd ->
        lexicon_status,metasenv,cmd
    | GrafiteAst.Obj (loc,obj) ->

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 742e538febd09a0f50b3780a319ac3d67a08c81d..396567a2e708f8b08bdc2972774c606738b5191c 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -664,7 +664,7 @@ EXTEND
           in
           L.Number_alias (instance, dsc)
       ]
-    ];
+     ];
     argument: [
       [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
         id = IDENT ->
@@ -785,6 +785,27 @@ EXTEND
             ind_types
         in
         G.NObj (loc, N.Inductive (params, ind_types))
+    | IDENT "universe"; IDENT "constraint"; u1 = tactic_term; 
+        strict = [ SYMBOL <:unicode<lt>> -> true 
+                 | SYMBOL <:unicode<leq>> -> false ]; 
+        u2 = tactic_term ->
+        let u1 =
+          match u1 with
+          | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
+              NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
+          | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
+              NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
+          | _ -> raise (Failure "only a sort can be constrained")
+        in
+        let u2 =
+          match u2 with
+          | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
+              NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
+          | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
+              NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
+          | _ -> raise (Failure "only a sort can be constrained")
+        in
+         G.NUnivConstraint (loc, strict,u1,u2)
     | IDENT "coercion" ; 
       t = [ u = URI -> N.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
       arity = OPT int ; saturations = OPT int; 

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);
 
 ;;
+*)
 

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index f31c4e9b1ebbc71416ced0dbbc120e4bf60c7448..4d60e5d42948f4729d2d0fef14e951c65985f554 100644 (file)
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -29,6 +29,16 @@ let max l1 l2 =
 
 let le_constraints = ref [] (* strict,a,b *)
 
+let resolve_universe u =
+  HExtlib.list_findopt 
+    (fun (_,a,b) _ -> 
+      prerr_endline (NUri.name_of_uri a);
+           if NUri.name_of_uri a = u then Some a 
+      else if NUri.name_of_uri b = u then Some b
+      else None) 
+    !le_constraints
+;;
+
 let rec le_path_uri avoid strict a b =
  (not strict && NUri.eq a b) ||
  List.exists

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli
index 4604bd2fdf2fe4a49537862fe88fc3f53f2ebf9b..c4fa396cc1d6d493afb4d80644c3b818e0cc2eda 100644 (file)
--- a/helm/software/components/ng_kernel/nCicEnvironment.mli
+++ b/helm/software/components/ng_kernel/nCicEnvironment.mli
@@ -33,6 +33,8 @@ val add_constraint: bool -> NCic.universe -> NCic.universe -> unit
 val sup : NCic.universe -> NCic.universe option
 val pp_constraints: unit -> string
 
+val resolve_universe: string -> NUri.uri option
+
 val get_checked_def:
   NReference.reference -> 
     NCic.relevance * string * NCic.term * NCic.term * NCic.c_attr * int

diff --git a/helm/software/components/ng_tactics/.depend b/helm/software/components/ng_tactics/.depend
index 2e34a62a912ffa6c454814fd5e8f2527b028617b..3ce24c446494b9e6e9690f964366bd16736d9e4f 100644 (file)
--- a/helm/software/components/ng_tactics/.depend
+++ b/helm/software/components/ng_tactics/.depend
@@ -1,6 +1,6 @@
-nTacStatus.cmi: 
 nTactics.cmi: nTacStatus.cmi 
-nCicElim.cmi: 
+nCicTacReduction.cmo: nCicTacReduction.cmi 
+nCicTacReduction.cmx: nCicTacReduction.cmi 
 nTacStatus.cmo: nCicTacReduction.cmi nTacStatus.cmi 
 nTacStatus.cmx: nCicTacReduction.cmx nTacStatus.cmi 
 nTactics.cmo: nTacStatus.cmi nTactics.cmi 

diff --git a/helm/software/components/ng_tactics/.depend.opt b/helm/software/components/ng_tactics/.depend.opt
index 2e34a62a912ffa6c454814fd5e8f2527b028617b..3ce24c446494b9e6e9690f964366bd16736d9e4f 100644 (file)
--- a/helm/software/components/ng_tactics/.depend.opt
+++ b/helm/software/components/ng_tactics/.depend.opt
@@ -1,6 +1,6 @@
-nTacStatus.cmi: 
 nTactics.cmi: nTacStatus.cmi 
-nCicElim.cmi: 
+nCicTacReduction.cmo: nCicTacReduction.cmi 
+nCicTacReduction.cmx: nCicTacReduction.cmi 
 nTacStatus.cmo: nCicTacReduction.cmi nTacStatus.cmi 
 nTacStatus.cmx: nCicTacReduction.cmx nTacStatus.cmi 
 nTactics.cmo: nTacStatus.cmi nTactics.cmi 

diff --git a/helm/software/matita/tests/ng_commands.ma b/helm/software/matita/tests/ng_commands.ma
index cbb73844d98b7d4fe55d8327d4ac9d57919930d1..2241043a9fe05d09f723d02ba1f0ef54c3714bdc 100644 (file)
--- a/helm/software/matita/tests/ng_commands.ma
+++ b/helm/software/matita/tests/ng_commands.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "nat/plus.ma".
+include "ng_pts.ma".
 
 ndefinition thesis0: ∀A:Type.Type ≝ λA. A → A.
 
@@ -30,6 +30,8 @@ naxiom NP: Prop.
 
 ndefinition Q: Prop ≝ NP.
 
+include "nat/nat.ma".
+
 nlet rec nzero (n:nat) : nat ≝
  match n with
   [ O ⇒ O
@@ -57,4 +59,4 @@ and nmzero (m:mat 0 (dt ?)) : nnat 0 (dt ?) ≝
  [ mS n ⇒ nnzero n ].
 
 nrecord pair (n: nat) (x: DT n) (label: Type): Type ≝
- { lbl:label; l: pair n x label; r: pair n x label}.
\ No newline at end of file
+ { lbl:label; l: pair n x label; r: pair n x label}.

diff --git a/helm/software/matita/tests/ng_elim.ma b/helm/software/matita/tests/ng_elim.ma
index dfded53ee2ed82759aa93e1b078c40c0d9018806..c8998a22795d4b63a3e8e45c3f4626fe7dd7ef68 100644 (file)
--- a/helm/software/matita/tests/ng_elim.ma
+++ b/helm/software/matita/tests/ng_elim.ma
@@ -12,6 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ng_pts.ma".
+
 ninductive nat: Type ≝
    O: nat
  | S: nat → nat.

diff --git a/helm/software/matita/tests/ng_pts.ma b/helm/software/matita/tests/ng_pts.ma
new file mode 100644 (file)
index 0000000..24606b8
--- /dev/null
+++ b/helm/software/matita/tests/ng_pts.ma
@@ -0,0 +1,24 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+universe constraint Type[0] < Type[1].
+universe constraint Type[1] < Type[2].
+universe constraint CProp[0] < CProp[1].
+universe constraint CProp[1] < CProp[2].
+universe constraint Type[0] ≤ CProp[0].
+universe constraint CProp[0] ≤ Type[0].
+universe constraint Type[1] ≤ CProp[1].
+universe constraint CProp[1] ≤ Type[1].
+universe constraint Type[2] ≤ CProp[2].
+universe constraint CProp[2] ≤ Type[2].
\ No newline at end of file

diff --git a/helm/software/matita/tests/ng_tactics.ma b/helm/software/matita/tests/ng_tactics.ma
index 6c7e161f68d6ea8692024d874e9f697ffdd057a1..3bb4a6fa4c8b3e3fd5ebe176546b1bd0d23f2f23 100644 (file)
--- a/helm/software/matita/tests/ng_tactics.ma
+++ b/helm/software/matita/tests/ng_tactics.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ng_pts.ma".
 include "nat/plus.ma".
 
 ntheorem test1 : ∀n:nat.n = S n + n → S n = (S (S n)).