From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 7 Jun 2005 17:37:16 +0000 (+0000)
Subject: added coercions
X-Git-Tag: PRE_INDEX_1~48
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ec6b4df6d02ff30a7a1cd784831017b05b1d46dd;p=helm.git

added coercions
---

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 99b7018e4..26a0f2487 100644
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -93,8 +93,13 @@ let eval_with_engine status user_goal parsed_text st =
     let module UM = UriManager in
     DTE.fold (
       fun k ((v,_) as value) acc -> 
-        let v = UM.strip_xpointer (UM.uri_of_string v) in
-        if List.exists (fun (s,_) -> s = v) new_status.objects then
+        let b = 
+          try
+            let v = UM.strip_xpointer (UM.uri_of_string v) in
+            List.exists (fun (s,_) -> s = v) new_status.objects 
+          with UM.IllFormedUri _ -> false
+        in
+        if b then 
           acc
         else
           DTE.add k value acc
diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index fbcac945a..9a44742b7 100644
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -170,21 +170,25 @@ let delta_status status1 status2 =
   in
   diff status1.objects status2.objects
 
+let remove_coercion uri = 
+  CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri)
+  
 let time_travel ~present ~past =
   let list_of_objs_to_remove = List.rev (delta_status past present) in
     (* List.rev is just for the debugging code, which otherwise may list both
     * something.ind and something.ind#xpointer ... (ask Enrico :-) *)
   let debug_list = ref [] in
-  List.iter (fun (x,p) -> 
-    remove_object_from_disk x p;
+  List.iter (fun (uri,p) -> 
+    remove_object_from_disk uri p;
+    remove_coercion uri;
     (try 
-      CicEnvironment.remove_obj x
+      CicEnvironment.remove_obj uri
     with CicEnvironment.Object_not_found _ -> 
       MatitaLog.debug
         (sprintf "time_travel removes from cache %s that is not in" 
-          (UriManager.string_of_uri x)));
-    let l = MatitaDb.remove_uri x in
-    debug_list := UriManager.string_of_uri x :: !debug_list @ l) 
+          (UriManager.string_of_uri uri)));
+    let l = MatitaDb.remove_uri uri in
+    debug_list := UriManager.string_of_uri uri :: !debug_list @ l) 
   list_of_objs_to_remove;
   
   (* this is debug code
diff --git a/helm/matita/tests/fix_betareduction.ma b/helm/matita/tests/fix_betareduction.ma
new file mode 100644
index 000000000..32f298d60
--- /dev/null
+++ b/helm/matita/tests/fix_betareduction.ma
@@ -0,0 +1,8 @@
+alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
+alias id "n" = "cic:/Suresnes/BDD/canonicite/Canonicity_BDT/n.con".
+alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
+theorem a: 
+  (\forall p: nat \to Prop.
+  \forall n: nat. p n \to p n ) \to (eq nat n n).
+intro.
+apply (H (\lambda n:nat.(eq nat n n))).
\ No newline at end of file
diff --git a/helm/matita/tests/match_inference.ma b/helm/matita/tests/match_inference.ma
new file mode 100644
index 000000000..a84b3c373
--- /dev/null
+++ b/helm/matita/tests/match_inference.ma
@@ -0,0 +1,17 @@
+inductive pos: Set \def
+| one : pos
+| next : pos \to pos.
+
+inductive nat:Set \def
+| O : nat
+| S : nat \to nat.
+
+inductive empty : Set \def .
+
+definition pos2nat : pos \to nat  \def 
+     \lambda x:pos . match x with  
+      [ one \Rightarrow O 
+      | (next z) \Rightarrow O]. 
+
+definition empty2nat : empty \to nat  \def
+  \lambda x : empty . S (match x in empty with []).
\ No newline at end of file
diff --git a/helm/matita/tests/mysql_escaping.ma b/helm/matita/tests/mysql_escaping.ma
new file mode 100644
index 000000000..798ab2786
--- /dev/null
+++ b/helm/matita/tests/mysql_escaping.ma
@@ -0,0 +1,3 @@
+theorem a' : Prop \to Prop.intros.assumption.qed.
+
+