fix

diff --git a/helm/matita/tests/apply.ma b/helm/matita/tests/apply.ma
new file mode 100644 (file)
index 0000000..9e86635
--- /dev/null
+++ b/helm/matita/tests/apply.ma
@@ -0,0 +1,24 @@
+%% test _with_ the WHD on the apply argument
+
+alias id "not" = "cic:/Coq/Init/Logic/not.con".
+alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)".
+
+theorem b:
+  \forall x:Prop.
+  (not x) \to x \to False.
+intro.
+apply H.
+assumption.
+qed.
+
+%% test _without_ the WHD on the apply argument
+
+alias symbol "eq" (instance 0) = "leibnitz's equality".
+
+theorem a:
+  \forall A:Set.
+  \forall x,y : A.
+  not (x=y) \to not (x=y).
+intro.
+apply H.
+qed.

diff --git a/helm/matita/tests/simpl.ma b/helm/matita/tests/simpl.ma
index 887566f5895fabc3b08b620edf4d3ced391b5272..c455b7692b3f9f7228afb8790239f8c9334e65af 100644 (file)
--- a/helm/matita/tests/simpl.ma
+++ b/helm/matita/tests/simpl.ma
@@ -5,4 +5,4 @@ theorem a :
  \forall x,y : A.
  not (x = y) \to not(y = x).
 intro.
-simplify in hyp not(x=y).
+simplify.