X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fassembly%2Fexadecimal.ma;h=fb1a14ede914299c6b2e9342296e846c39dc54b0;hb=03c219fd478b4160ef1bc0b9e66520afeb6394ac;hp=7dfd42bb117af8111b6efd1ee1c81a3242c5a709;hpb=d27cfdc825df15aade7edd457b08ee614d44aa32;p=helm.git

diff --git a/helm/software/matita/library/assembly/exadecimal.ma b/helm/software/matita/library/assembly/exadecimal.ma
index 7dfd42bb1..fb1a14ede 100644
--- a/helm/software/matita/library/assembly/exadecimal.ma
+++ b/helm/software/matita/library/assembly/exadecimal.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/assembly/exadecimal/".
 
-include "extra.ma".
+include "assembly/extra.ma".
 
 inductive exadecimal : Type ≝
    x0: exadecimal
@@ -927,4 +927,4 @@ lemma xpred_S: ∀b. xpred (exadecimal_of_nat (S b)) = exadecimal_of_nat b.
  intros;
  rewrite > exadecimal_of_nat_mod;
  rewrite > exadecimal_of_nat_mod in ⊢ (? ? ? %);
-*)
\ No newline at end of file
+*)