Change (or better define) the order of hints premises.

[helm.git] / helm / software / matita / nlibrary / hints_declaration.ma

diff --git a/helm/software/matita/nlibrary/hints_declaration.ma b/helm/software/matita/nlibrary/hints_declaration.ma
index 3df2db00194aa05d43e8073f1be6e4121dd5af3d..99aca7fa6e79fe01a6f086cded9bbc146b309a9a 100644 (file)
--- 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! *)