Conflicting definitions of - - ?

[GoogleCodeExporter]

What steps will reproduce the problem?
1. load ocaml and hol.ml as usual
2. loadt "Library/analysis.ml";;
3. loadt "Multivariate/vectors.ml";;

What is the expected output? What do you see instead?
Expecting exit with no problems.  Instead, it exits with the final lines:

val DOT_RMUL : thm = |- !c x y. x dot c % y = c * (x dot y)
Warning: inventing type variables
Exception: Failure "GEN_TAC".
Error in included file 
/home/ivan/Dropbox/ReadSterling/hol_light/Multivariate/vectors.ml
val it : unit = ()

What version of the product are you using? On what operating system?
2.20++ , Linux Mint

Please provide any additional information below.

It appears that the "--" defined in analysis.ml conflicts somehow with the "--" 
defined in realax.ml , or I may be completely off.

Original issue reported on code.google.com by isterl...@smcm.edu on 2 Mar 2014 at 10:52

[GoogleCodeExporter]

In general, the Multivariate theories are not compatible with the older
analysis theories. I'd recommend using the full multivariate analysis theory
instead (see for example Multivariate/make_complex.ml). This is a lot more
heavyweight but gives a much more comprehensive analytical theory, and it's
built on top of Multivariate/vectors.ml.

Original comment by jrh...@gmail.com on 9 Mar 2014 at 4:56

[GoogleCodeExporter]

Thank you for the advice.  I had come to more or less similar
conclusions and I'm attempting to change and/or reorder my code
accordingly.

Original comment by isterl...@smcm.edu on 11 Mar 2014 at 3:30