X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fhints_declaration.ma;h=99aca7fa6e79fe01a6f086cded9bbc146b309a9a;hb=7d7f1e8403bebcfc759d0955bd2f5a4837c414b2;hp=3df2db00194aa05d43e8073f1be6e4121dd5af3d;hpb=e8fbe5898b3214a5b0c4d48e8c9d1ee55f3415cc;p=helm.git

diff --git a/helm/software/matita/nlibrary/hints_declaration.ma b/helm/software/matita/nlibrary/hints_declaration.ma
index 3df2db001..99aca7fa6 100644
--- a/helm/software/matita/nlibrary/hints_declaration.ma
+++ b/helm/software/matita/nlibrary/hints_declaration.ma
@@ -34,6 +34,9 @@ With unidoce and some ASCII art it looks like the following:
  (*---------------------*) ⊢
          T1 ≡ T2       
 
+The order of premises is relevant, since they are processed in order
+(left to right).
+
 *)
    
 (* it seems unbelivable, but it works! *)