]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/tests/hard_refine.ma
procedural: added fwd rewrite in arbitrary proofs (not just premises)
[helm.git] / matita / tests / hard_refine.ma
index 1b194559c28b97918b8d184c57027f1aab23c9e9..94766ab0b06ba67c81c31ac3d65c1a1dfb8aeb81 100644 (file)
@@ -1,5 +1,5 @@
 set "baseuri" "cic:/matita/TPTP/BOO024-1".
-include "legacy/coq.ma".
+include "../legacy/coq.ma".
 alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
 (* Inclusion of: BOO024-1.p *)
 (* -------------------------------------------------------------------------- *)