now baseuri is needed in each file (and its redefinition is forbidden)

[helm.git] / helm / matita / tests / inversion.ma

diff --git a/helm/matita/tests/inversion.ma b/helm/matita/tests/inversion.ma
index e61e123d791d687bbc0323ea5f16fc0aa6f6c25a..5f173344454084a0f2fd296b9732d4ba2f16729c 100644 (file)
--- a/helm/matita/tests/inversion.ma
+++ b/helm/matita/tests/inversion.ma
@@ -1,3 +1,5 @@
+set "baseuri" "cic:/matita/tests/".
+
 inductive nat : Set \def
    O : nat
  | S : nat \to nat.
@@ -19,4 +21,4 @@ theorem test_inversion: \forall n. le n O \to n=O.
   intro. reflexivity.
   simplify. intros.
   discriminate H3.
-qed.
\ No newline at end of file
+qed.