first snapshot of separate compilation

diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in
index 168dfa3051ec78d1f85a60b81c9f79d2b3d4ffdc..bed070a5113122562e7824f2489c90746582f15e 100644 (file)
--- a/helm/matita/Makefile.in
+++ b/helm/matita/Makefile.in
@@ -107,7 +107,8 @@ clean:
        rm -rf *.cma *.cmo *.cmi *.cmx *.cmxa *.a *.o   \
                matita matita.opt matitac matitac.opt   \
                cicbrowser cicbrowser.opt       \
-               matitadep matitadep.opt
+               matitadep matitadep.opt \
+               matitaclean matitaclean.opt
 distclean: clean
        rm -f matitaGeneratedGui.ml matitaGeneratedGui.mli
        rm -f config.log config.status Makefile buildTimeConf.ml

diff --git a/helm/matita/Makefile.tests b/helm/matita/Makefile.tests
new file mode 100644 (file)
index 0000000..cab6702
--- /dev/null
+++ b/helm/matita/Makefile.tests
@@ -0,0 +1,40 @@
+TODO=\
+       tests/apply.moo\
+       tests/auto.moo\
+       tests/baseuri.moo\
+       tests/coercions.moo\
+       tests/comments.moo\
+       tests/fguidi.moo\
+       tests/first.moo\
+       tests/fix_betareduction.moo\
+       tests/inversion.moo\
+       tests/letrec.moo\
+       tests/match.moo\
+       tests/match_inference.moo\
+       tests/mysql_escaping.moo\
+       tests/record.moo\
+       tests/replace.moo\
+       tests/rewrite.moo\
+       tests/second.moo\
+       tests/simpl.moo\
+       tests/test2.moo\
+       tests/test3.moo\
+       tests/test4.moo\
+       tests/third.moo
+
+DEPEND_NAME=.depend.moo
+
+all: $(TODO)
+
+clean:
+       rm -f $(DEPEND_NAME) $(TODO) 
+       ./matitaclean all
+
+%.moo:%.ma
+       [ ! -e $@ ] || ./matitaclean $< 
+       ./matitac $< || ./matitaclean $<
+
+$(DEPEND_NAME): $(TODO:%.moo=%.ma)
+       ./matitadep $^ > $@
+
+include $(DEPEND_NAME)

diff --git a/helm/matita/matita.lang b/helm/matita/matita.lang
index 439440710b29ef8edf95eeb589ca8e85af35dd11..f74da76e74f3cab07d94f93a6f3df70336eb1cfe 100644 (file)
--- a/helm/matita/matita.lang
+++ b/helm/matita/matita.lang
@@ -28,6 +28,7 @@
     <keyword>coinductive</keyword>
     <keyword>corec</keyword>
     <keyword>in</keyword>
+    <keyword>on</keyword>
     <keyword>inductive</keyword>
     <keyword>let</keyword>
     <keyword>match</keyword>

diff --git a/helm/matita/matitaDb.ml b/helm/matita/matitaDb.ml
index c5bdbf84befc7dcbf595ed0a5d633b348108acea..17aac37450cf091faad1fbaced5d1589eb89f408 100644 (file)
--- a/helm/matita/matitaDb.ml
+++ b/helm/matita/matitaDb.ml
@@ -150,3 +150,14 @@ let remove_uri uri =
   with
     exn -> raise exn (* no errors should be accepted *)
 
+let xpointers_of_ind uri =
+  let dbd = instance () in
+  let name_tbl =  MetadataTypes.name_tbl () in
+  let query = sprintf 
+    "SELECT source FROM %s WHERE source LIKE '%s#xpointer%%'" name_tbl 
+      (Mysql.escape (UriManager.string_of_uri uri))
+  in
+  let rc = Mysql.exec dbd query in
+  let l = ref [] in
+  Mysql.iter rc (fun a ->  match a.(0) with None ->()|Some a -> l := a:: !l);
+  List.map UriManager.uri_of_string !l

diff --git a/helm/matita/matitaDb.mli b/helm/matita/matitaDb.mli
index 112b2d0b246d219f5cce031ecdbfa5ec993d77b2..3b3bd58c10c8762add96f20f984893e6d2fd2d7b 100644 (file)
--- a/helm/matita/matitaDb.mli
+++ b/helm/matita/matitaDb.mli
@@ -29,3 +29,4 @@ val clean_owner_environment : unit -> unit
 val create_owner_environment : unit -> unit 
 
 val remove_uri: UriManager.uri -> string list
+val xpointers_of_ind: UriManager.uri -> UriManager.uri list

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 42e8f1c404f0747552a2ffb3f2dda8b5b809457e..660be6c10b76856a78fef83800945ccbf16ee03e 100644 (file)
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -223,8 +223,31 @@ let alias_diff ~from status =
     status.aliases Map.empty
 
 let remove uri =
-  let path = Http_getter.resolve' uri in
-  remove_object_from_disk uri path;
-  remove_coercion uri;
-  ignore(MatitaDb.remove_uri uri)
+  let derived_uris_of_uri uri =
+    UriManager.innertypesuri_of_uri uri ::
+    UriManager.annuri_of_uri uri ::
+    (match UriManager.bodyuri_of_uri uri with
+    | None -> []
+    | Some u -> [u])
+  in
+  let to_remove =
+    uri :: 
+    (if UriManager.uri_is_ind uri then MatitaDb.xpointers_of_ind uri else []) @
+    derived_uris_of_uri uri   
+  in   
+  List.iter 
+    (fun uri -> 
+      (try
+        let path = 
+          let path = Http_getter.resolve' (UriManager.strip_xpointer uri) in
+          assert (String.sub path 0 7 = "file://");
+          String.sub path 7 (String.length path - 7)
+        in
+        remove_object_from_disk uri path; 
+      with
+        Http_getter_types.Key_not_found _ -> Http_getter.unregister' uri);
+      remove_coercion uri; 
+      ignore(MatitaDb.remove_uri uri))
+  to_remove
+  
   

diff --git a/helm/matita/matitaSync.mli b/helm/matita/matitaSync.mli
index 0c866d4e59ada70cb362293535fbc406d0f90213..376ba37949e0f6ed848492f5f06506207d8213f8 100644 (file)
--- a/helm/matita/matitaSync.mli
+++ b/helm/matita/matitaSync.mli
@@ -36,6 +36,8 @@ val time_travel:
 val alias_diff: from:MatitaTypes.status -> MatitaTypes.status ->
   DisambiguateTypes.environment
 
-  (* removes the object from DB, Disk, CoercionsDB *)
+  (* removes the object from DB, Disk, CoercionsDB, getter 
+   * asserts the uri is resolved to file:// so it is only for 
+   * user's objects *)
 val remove: UriManager.uri -> unit
 

diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index ea8888eb706c3fda00f39823bf129626b8308794..5f07aa406df52c7007c9f8e3d0f97636d8fd33a1 100644 (file)
--- a/helm/matita/matitacLib.ml
+++ b/helm/matita/matitacLib.ml
@@ -103,8 +103,10 @@ let main ~mode =
   Helm_registry.load_from "matita.conf.xml";
   Http_getter.init ();
   MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
+(*
   MatitaDb.clean_owner_environment ();
   MatitaDb.create_owner_environment ();
+*)
   status := Some (ref (Lazy.force MatitaEngine.initial_status));
   at_exit
     (fun () ->

diff --git a/helm/matita/matitaclean.ml b/helm/matita/matitaclean.ml
index 60292515ae11b598856128822507ece6f925c946..eb0c5787d3e0fbaac1d4a01907013385bb12e6b1 100644 (file)
--- a/helm/matita/matitaclean.ml
+++ b/helm/matita/matitaclean.ml
@@ -1,6 +1,7 @@
 module HGT = Http_getter_types;;
 module HG = Http_getter;;
 module UM = UriManager;;
+module TA = TacticAst;;
 
 let _ =
   Helm_registry.load_from "matita.conf.xml";
@@ -13,34 +14,49 @@ let clean_all () =
   exit 0
   
 let dbd = MatitaDb.instance ()
+let cache_of_processed_baseuri = Hashtbl.create 1024
 
 let one_step_depend suri =
-  let dbg_q = 
-    let suri = Mysql.escape suri in
-    (**** FIX FIX FIX ***)
-    (****** let obj_tbl = MetadataTypes.obj_tbl () in  ******)
-    let obj_tbl = MetadataTypes.library_obj_tbl in 
-    (**** FIX FIX FIX ***)
-    Printf.sprintf 
-      "SELECT source FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl suri
+  let buri =
+    try
+      UM.buri_of_uri (UM.uri_of_string suri)
+    with UM.IllFormedUri _ -> suri
   in
-  try 
-    let rc = Mysql.exec dbd dbg_q in
-    let l = ref [] in
-    Mysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l := a:: !l);
-    let l = List.sort Pervasives.compare !l in
-    MatitaMisc.list_uniq l
-  with
-    exn -> raise exn (* no errors should be accepted *)
+  if Hashtbl.mem cache_of_processed_baseuri buri then 
+    []
+  else
+    begin
+      Hashtbl.add cache_of_processed_baseuri buri true;
+      let query = 
+        let buri = buri ^ "/" in 
+        let buri = Mysql.escape buri in
+        let obj_tbl = MetadataTypes.obj_tbl () in
+        Printf.sprintf 
+          "SELECT source FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl buri
+      in
+      try 
+        let rc = Mysql.exec dbd query in
+        let l = ref [] in
+        Mysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l:=a:: !l);
+        let l = List.sort Pervasives.compare !l in
+        MatitaMisc.list_uniq l
+      with
+        exn -> raise exn (* no errors should be accepted *)
+    end
 
-let cache_of_processed_baseuri = Hashtbl.create 1024
     
+let safe_buri_of_suri suri =
+  try
+    UM.buri_of_uri (UM.uri_of_string suri)
+  with
+    UM.IllFormedUri _ -> suri
+
 let close_uri_list uri_to_remove =
   (* to remove an uri you have to remove the whole script *)
   let buri_to_remove = 
     MatitaMisc.list_uniq 
       (List.fast_sort Pervasives.compare 
-        (List.map UM.buri_of_uri uri_to_remove))
+        (List.map safe_buri_of_suri uri_to_remove))
   in
   (* cleand the already visided baseuris *)
   let buri_to_remove = 
@@ -50,9 +66,6 @@ let close_uri_list uri_to_remove =
         else true)
       buri_to_remove
   in
-  List.iter 
-    (fun buri -> Hashtbl.add cache_of_processed_baseuri buri true)
-    buri_to_remove;
   (* now calculate the list of objects that belong to these baseuris *)
   let uri_to_remove = 
     List.fold_left 
@@ -64,7 +77,7 @@ let close_uri_list uri_to_remove =
         in
         let inhabitants = List.map 
             (function 
-             | HGT.Ls_object e -> UM.uri_of_string (buri ^ "/" ^ e.HGT.uri) 
+             | HGT.Ls_object e -> buri ^ "/" ^ e.HGT.uri 
              | _ -> assert false)
           inhabitants
         in
@@ -74,15 +87,27 @@ let close_uri_list uri_to_remove =
   (* now we want the list of all uri that depend on them *) 
   let depend = 
     List.fold_left
-    (fun acc u -> one_step_depend (UM.string_of_uri u) @ acc) [] uri_to_remove
+    (fun acc u -> one_step_depend u @ acc) [] uri_to_remove
   in
   let depend = 
     MatitaMisc.list_uniq 
       (List.fast_sort Pervasives.compare depend) 
   in
-  let depend = List.map UM.uri_of_string depend in
   uri_to_remove, depend
 
+let buri_of_file file = 
+  let ic = open_in file in
+  let stms = CicTextualParser2.parse_statements (Stream.of_channel ic) in
+  close_in ic;
+  let uri = ref "" in
+  List.iter 
+    (function
+    | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", buri))) ->
+        uri := MatitaMisc.strip_trailing_slash buri
+    | _ -> ()) 
+    stms;
+  !uri
+
 let main uri_to_remove =
   let rec fix uris next =
     match next with
@@ -96,8 +121,8 @@ let usage () =
   prerr_endline "";
   prerr_endline "usage:";
   prerr_endline "\tmatitaclean all";
-  prerr_endline "\tmatitaclean dry uris...";
-  prerr_endline "\tmatitaclean uris...";
+  prerr_endline "\tmatitaclean dry (uri|file)+";
+  prerr_endline "\tmatitaclean (uri|file)+";
   prerr_endline "";
   exit 1
     
@@ -113,24 +138,31 @@ let _ =
     if Sys.argv.(1) = "dry" then 2, true else 1, false
   in
   let uri_to_remove =ref [] in
-  try 
+  (try 
     for i = start to Array.length Sys.argv - 1 do
       let suri = Sys.argv.(i) in
-      let uri = UM.uri_of_string suri in
+      let uri = 
+        try
+          UM.buri_of_uri (UM.uri_of_string suri)
+        with
+          UM.IllFormedUri _ -> buri_of_file suri
+      in
       uri_to_remove := uri :: !uri_to_remove
     done
   with
-    Invalid_argument _ -> usage ();
+    Invalid_argument _ -> usage ());
   let l = main !uri_to_remove in
   if dry then
     begin
-      List.iter (fun x -> let u = UM.string_of_uri x in prerr_endline u) l;
+      List.iter prerr_endline l;
       exit 0
     end
   else
     List.iter 
       (fun u ->
-        prerr_endline ("Removing " ^ UM.string_of_uri u);
-        MatitaSync.remove u)
+        prerr_endline ("Removing " ^ u);
+        try
+          MatitaSync.remove (UM.uri_of_string u)
+        with Sys_error _ -> ())
     l
   

diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml
index df6cff2734598cb78fe9c16e9a795db538aaf141..c1ccce7808c9cdacc1c79baa21bcb96460efc562 100644 (file)
--- a/helm/matita/matitadep.ml
+++ b/helm/matita/matitadep.ml
@@ -27,20 +27,26 @@ let main () =
   for i = 1 to Array.length Sys.argv - 1 do
     let file = Sys.argv.(i) in
     let ic = open_in file in
-    let stms = CicTextualParser2.parse_statements (Stream.of_channel ic) in
-    close_in ic;
-    let stms = 
-      List.iter 
-        (function
-        | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", uri))) ->
-            let uri = MatitaMisc.strip_trailing_slash uri in
-            baseuri := (uri, file) :: !baseuri
-        | TA.Executable (_, TA.Command 
-            (_, TA.Alias (_, TA.Ident_alias(_, uri)))) -> 
-              Hashtbl.add aliases file uri
-        | _ -> ()) 
-      stms 
+    let stms =
+      try
+        CicTextualParser2.parse_statements (Stream.of_channel ic)
+      with
+        (CicTextualParser2.Parse_error _) as exc ->
+          prerr_endline ("Unable to parse: " ^ file);
+          prerr_endline (MatitaExcPp.to_string exc);
+          exit 1
     in
+    close_in ic;
+    List.iter 
+      (function
+      | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", uri))) ->
+          let uri = MatitaMisc.strip_trailing_slash uri in
+          baseuri := (uri, file) :: !baseuri
+      | TA.Executable (_, TA.Command 
+          (_, TA.Alias (_, TA.Ident_alias(_, uri)))) -> 
+            Hashtbl.add aliases file uri
+      | _ -> ()) 
+      stms; 
     Hashtbl.iter 
       (fun file alias -> 
         let dep = resolve alias in

diff --git a/helm/matita/tests/apply.ma b/helm/matita/tests/apply.ma
index 09b80cd4ee15234d16ace68adb7fd471a6bd8a70..e53d315f0339c8dd2053bf3203685cbd7ff06c25 100644 (file)
--- a/helm/matita/tests/apply.ma
+++ b/helm/matita/tests/apply.ma
@@ -1,5 +1,5 @@
 (* test _with_ the WHD on the apply argument *)
-set "baseuri" "cic:/matita/tests/".
+set "baseuri" "cic:/matita/tests/apply/".
 
 alias id "not" = "cic:/Coq/Init/Logic/not.con".
 alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)".

diff --git a/helm/matita/tests/auto.ma b/helm/matita/tests/auto.ma
index c6b525b2b087a236f75b71ee22f0a1597b0cf4ab..66b973cfd5b27197fbba6fa681570492109d3fb0 100755 (executable)
--- a/helm/matita/tests/auto.ma
+++ b/helm/matita/tests/auto.ma
@@ -1,4 +1,4 @@
-set "baseuri" "cic:/matita/tests/".
+set "baseuri" "cic:/matita/tests/auto/".
 
 alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
 alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".

diff --git a/helm/matita/tests/baseuri.ma b/helm/matita/tests/baseuri.ma
index 3715a268a16bd23f9116642a8ccd3e339437ca88..eb4ae6a68b9718b950aa50181c0d97e7b72dd522 100644 (file)
--- a/helm/matita/tests/baseuri.ma
+++ b/helm/matita/tests/baseuri.ma
@@ -1,2 +1,2 @@
-set "baseuri" "cic:/matita/tests/".
-set "baseuri" "cic:/matita/tests/".
+set "baseuri" "cic:/matita/tests/baseuri/".
+set "baseuri" "cic:/matita/tests/baseuri/".

diff --git a/helm/matita/tests/coercions.ma b/helm/matita/tests/coercions.ma
index 507147cef8b1802a925746acdec4b097a5bf07ca..2444b1d74a3a638dddb85a3b42cf84d11acf6a82 100644 (file)
--- a/helm/matita/tests/coercions.ma
+++ b/helm/matita/tests/coercions.ma
@@ -1,4 +1,4 @@
-set "baseuri" "cic:/matita/tests/".
+set "baseuri" "cic:/matita/tests/coercions/".
 
 inductive pos: Set \def
 | one : pos

diff --git a/helm/matita/tests/comments.ma b/helm/matita/tests/comments.ma
index 3e3ec9d5e985d933efb4747ea512d30968c9ab9d..cd21535e7213a671e1a0307aa5bc8cc8d91a2d5e 100644 (file)
--- a/helm/matita/tests/comments.ma
+++ b/helm/matita/tests/comments.ma
@@ -12,7 +12,7 @@
 (*                                                                          *)
 (****************************************************************************)
 
-set "baseuri" "cic:/matita/tests/".
+set "baseuri" "cic:/matita/tests/comments/".
 
 (* commento che va nell'ast, ma non viene contato
     come step perche' non e' un executable

diff --git a/helm/matita/tests/fguidi.ma b/helm/matita/tests/fguidi.ma
index fc2c717eba684ff02a14ef0f1819e8956238d7e0..e42de00b50a9a530542696c461ae945caaa2459f 100644 (file)
--- a/helm/matita/tests/fguidi.ma
+++ b/helm/matita/tests/fguidi.ma
@@ -1,4 +1,4 @@
-set "baseuri" "cic:/matita/tests/".
+set "baseuri" "cic:/matita/tests/fguidi/".
 
 alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".

diff --git a/helm/matita/tests/first.ma b/helm/matita/tests/first.ma
new file mode 100644 (file)
index 0000000..d75f372
--- /dev/null
+++ b/helm/matita/tests/first.ma
@@ -0,0 +1,25 @@
+set "baseuri" "cic:/matita/tests/first/".
+
+inductive nat : Set \def
+  | O : nat
+  | S : nat \to nat.
+
+inductive eq (A:Set): A \to A \to Prop \def
+  refl: \forall x:A.eq A x x. 
+
+inductive list (A:Set) : Set \def
+  | nil : list A
+  | cons : A \to list A \to list A.
+alias symbol "cast" (instance 0) = "type cast".
+
+let rec list_len (A:Set) (l:list A) on l \def
+  [\lambda x.nat]
+  match (l:list A) with 
+  [ nil \Rightarrow O
+  | (cons a tl) \Rightarrow S (list_len A tl)].
+  
+theorem stupid: \forall A:Set.eq ? (list_len A (nil ?)) O.
+intros.
+normalize.
+apply refl.
+qed.

diff --git a/helm/matita/tests/fix_betareduction.ma b/helm/matita/tests/fix_betareduction.ma
index d86602c5748fe9e63a25a4056934945d9b417aba..b4ea8d8b510371aacc0eb638af9fb292f1ea3561 100644 (file)
--- a/helm/matita/tests/fix_betareduction.ma
+++ b/helm/matita/tests/fix_betareduction.ma
@@ -1,4 +1,4 @@
-set "baseuri" "cic:/matita/tests/".
+set "baseuri" "cic:/matita/tests/fix_betareduction/".
 
 alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
 alias id "n" = "cic:/Suresnes/BDD/canonicite/Canonicity_BDT/n.con".

diff --git a/helm/matita/tests/inversion.ma b/helm/matita/tests/inversion.ma
index 4ea9e2deb76d59940a50eab535d75cb202228818..c76851f59fa8dd1240d87fdb04d8072a5544ba5f 100644 (file)
--- a/helm/matita/tests/inversion.ma
+++ b/helm/matita/tests/inversion.ma
@@ -1,4 +1,4 @@
-set "baseuri" "cic:/matita/tests/".
+set "baseuri" "cic:/matita/tests/inversion/".
 
 inductive nat : Set \def
    O : nat

diff --git a/helm/matita/tests/letrec.ma b/helm/matita/tests/letrec.ma
index b47c5aebb3722514f536f268fad7c17b9516585b..e8e81fa014e0d0df11cefecbcfb015339894de04 100644 (file)
--- a/helm/matita/tests/letrec.ma
+++ b/helm/matita/tests/letrec.ma
@@ -1,4 +1,4 @@
-set "baseuri" "cic:/matita/tests/".
+set "baseuri" "cic:/matita/tests/letrec/".
 
 
 alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".

diff --git a/helm/matita/tests/match.ma b/helm/matita/tests/match.ma
index e36e684c2bba815d70f38d4c204e3310170b555b..f006a7045b1ece7beb50f02c7ccd31dbdd566852 100644 (file)
--- a/helm/matita/tests/match.ma
+++ b/helm/matita/tests/match.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/tests/".
+set "baseuri" "cic:/matita/tests/match/".
 
 
 inductive True: Prop \def

diff --git a/helm/matita/tests/match_inference.ma b/helm/matita/tests/match_inference.ma
index d5df929bbfb14f791f982875f29eb51296ca1fdb..5cfa19cc9d326b9fb82715f9962b6eaa934704bf 100644 (file)
--- a/helm/matita/tests/match_inference.ma
+++ b/helm/matita/tests/match_inference.ma
@@ -1,4 +1,4 @@
-set "baseuri" "cic:/matita/tests/".
+set "baseuri" "cic:/matita/tests/match_inference/".
 
 inductive pos: Set \def
 | one : pos

diff --git a/helm/matita/tests/mysql_escaping.ma b/helm/matita/tests/mysql_escaping.ma
index b8a6d9be778ed3801e13908677e62e746a4edecd..e1698abd2b6186b5d880226b5da1d0f2b2c69d38 100644 (file)
--- a/helm/matita/tests/mysql_escaping.ma
+++ b/helm/matita/tests/mysql_escaping.ma
@@ -1,4 +1,4 @@
-set "baseuri" "cic:/matita/tests/".
+set "baseuri" "cic:/matita/tests/mysql_escaping/".
 
 theorem a' : Prop \to Prop.intros.assumption.qed.
 

diff --git a/helm/matita/tests/record.ma b/helm/matita/tests/record.ma
index 96463f599ea8a0968b77f437e45242602c0f7b7e..02ef85a0504ddd2c939b2a69ffe752bc544caedd 100644 (file)
--- a/helm/matita/tests/record.ma
+++ b/helm/matita/tests/record.ma
@@ -1,4 +1,4 @@
-set "baseuri" "cic:/matita/tests/".
+set "baseuri" "cic:/matita/tests/record/".
 
 record empty : Type \def {}.
 

diff --git a/helm/matita/tests/rewrite.ma b/helm/matita/tests/rewrite.ma
index bf4f3a6e572b485f90171e0562bf1020b2fa577a..3941ab0cb4d1e1d53cbc0be4b6fc64a921864714 100644 (file)
--- a/helm/matita/tests/rewrite.ma
+++ b/helm/matita/tests/rewrite.ma
@@ -1,4 +1,4 @@
-set "baseuri" "cic:/matita/tests/".
+set "baseuri" "cic:/matita/tests/rewrite/".
 
 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
 alias num (instance 0) = "natural number".

diff --git a/helm/matita/tests/second.ma b/helm/matita/tests/second.ma
new file mode 100644 (file)
index 0000000..ef13fc1
--- /dev/null
+++ b/helm/matita/tests/second.ma
@@ -0,0 +1,10 @@
+set "baseuri" "cic:/matita/tests/second/".
+alias id "nat" = "cic:/matita/tests/first/nat.ind#xpointer(1/1)".
+alias id "O" = "cic:/matita/tests/first/nat.ind#xpointer(1/1/1)".
+alias id "eq" = "cic:/matita/tests/first/eq.ind#xpointer(1/1)".
+alias id "refl" = "cic:/matita/tests/first/eq.ind#xpointer(1/1/1)".
+
+theorem ultrastupid : eq nat O O.
+apply refl.
+qed.
+

diff --git a/helm/matita/tests/simpl.ma b/helm/matita/tests/simpl.ma
index d77f91fcd0974043b22bb1a55fe3a178f6016d53..3edc4cf35f986d54bd1ed36c02e5ab11f644091b 100644 (file)
--- a/helm/matita/tests/simpl.ma
+++ b/helm/matita/tests/simpl.ma
@@ -1,4 +1,4 @@
-set "baseuri" "cic:/matita/tests/".
+set "baseuri" "cic:/matita/tests/simpl/".
 
 alias id "not" = "cic:/Coq/Init/Logic/not.con".
 alias symbol "eq" (instance 0) = "leibnitz's equality".

diff --git a/helm/matita/tests/test2.ma b/helm/matita/tests/test2.ma
index d622703b42bbb6bc2d246620878447563dd2b6e5..cf265671072179f73e309c9ecba6a36a0b78bfb0 100644 (file)
--- a/helm/matita/tests/test2.ma
+++ b/helm/matita/tests/test2.ma
@@ -1,4 +1,4 @@
-set "baseuri" "cic:/matita/tests/".
+set "baseuri" "cic:/matita/tests/test2/".
 
 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
 alias symbol "and" (instance 0) = "logical and".

diff --git a/helm/matita/tests/test3.ma b/helm/matita/tests/test3.ma
index 08ca196829ec903829ee103ab3ec1bbb0380ac39..9a8958b2175360f26ab23ddadf7adad908725261 100644 (file)
--- a/helm/matita/tests/test3.ma
+++ b/helm/matita/tests/test3.ma
@@ -1,4 +1,4 @@
-set "baseuri" "cic:/matita/tests/".
+set "baseuri" "cic:/matita/tests/test3/".
 
 alias symbol "eq" (instance 0) = "leibnitz's equality".
 theorem a:\forall x.x=x.

diff --git a/helm/matita/tests/test4.ma b/helm/matita/tests/test4.ma
index e25472d3ca0fea11866a194a9364c7ca18524e52..be67f3a8eacd5793e4c124b21935125b3a3600fa 100644 (file)
--- a/helm/matita/tests/test4.ma
+++ b/helm/matita/tests/test4.ma
@@ -1,4 +1,4 @@
-set "baseuri" "cic:/matita/tests/".
+set "baseuri" "cic:/matita/tests/test4/".
 
 
 (* commento che va nell'ast, ma non viene contato

diff --git a/helm/matita/tests/third.ma b/helm/matita/tests/third.ma
new file mode 100644 (file)
index 0000000..e0ae453
--- /dev/null
+++ b/helm/matita/tests/third.ma
@@ -0,0 +1,10 @@
+set "baseuri" "cic:/matita/tests/third/".
+alias id "nat" = "cic:/matita/tests/first/nat.ind#xpointer(1/1)".
+alias id "O" = "cic:/matita/tests/first/nat.ind#xpointer(1/1/1)".
+alias id "eq" = "cic:/matita/tests/first/eq.ind#xpointer(1/1)".
+alias id "ultrastupid" = "cic:/matita/tests/second/ultrastupid.con".
+
+theorem iperstupid : eq nat O O.
+exact ultrastupid.
+qed.
+