| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| | |
Typically, a problem of the form "?x args = match ?y with ... end" was
a failure even if miller-unification was applicable.
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Renouncing to bypass the library path given by "camlp5o -where" what
we assume to be the default library location, considering that
-usecamlp5dir is here to deal with the non-standard installation
layout.
Renouncing to find camlp5 libraries in a subdirectory of the ocaml
library directory since we now know that camlp5o is found and that we
have a priori to trust option -where of camlp5o.
Additionally falling back on looking for camlp4 if a camlp5 library is
found but no camlp5 binary. Also using camlp5o as a reference since
after all this is camlp5o that we need.
In particular, this fixes situations where -usecamlp5dir is given but
"camlp5o -where" contradicts it.
If something has to be checked on windows, please tell.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Now, type_scope is consistently used whether it is an hypothesis or
the conclusion, and consistently not used when in "context".
The question of a compatibility support, e.g., as suggested by Jason,
using a scope is still open though.
See reports #3050 and #4398.
|
| | |
| |
| |
| |
| | |
on the contrary of message given in 23041481f, while it introduces a
square time complexity of the size of the goal in subterm finding.
|
| | | |
|
| |\ \ |
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The error message was not only causing coqtop to exit, but also coqide to
crash, which led to a rather poor user experience. Since the code does not
actually care about the file extension, this commit just removes the test.
|
| | | | | |
|
| |/ / / |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
grammar.cma is built by Makefile.build in a specific, hardcoded way.
Let's remove this old .mllib file to avoid potential confusions in
the future.
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
General idea : Makefile.build was far too big to be easy to grasp or
maintain, with information scattered everywhere. Let's try to tidy that!
Normally, this commit is transparent for the user. We simply regroup
some parts of Makefile.build in several new dedicated files:
- Makefile.ide
- Makefile.checker
- Makefile.dev (for printers, revision, extra partial targets, otags)
- Makefile.install
These new files are "included" at the start of Makefile.build, to provide
the same behavior as before, but with a Makefile.build shrinked by 50%
(to approx 600 lines). Makefile.build now handles in priority the build
of coqtop, minor tools, theories and plugins.
Note: this is *not* a separate build system for coqchk nor coqide,
even if this can be seen as a first step in this direction (won't be easy
anyway to continue, due to the sharing of various stuff in lib and more).
In particular Makefile.{coqchk,ide} may rely here and there on some generic
rules left in Mafefile.build. Conversely, be sure to prefix rules in
Makefile.{coqchk,ide} by checker/... or ide/... in order to avoid
interferences with generic rules.
Makefile.common is still there, but quite simplified. For instance,
some variables that were used only once (e.g. lists of cmo files to link
in the various tools) are now defined in Makefile.build, directly
where they're needed. THEORIESVO and PLUGINSVO are made directly out of
the theories/*/vo.itarget and plugins/*/vo.itarget files, no long manual
list of subdirs anymore. Specific sub-targets such as 'reals' still
exist, but in Makefile.dev, and they aren't mandatory.
Makefile.doc is augmented by the rules building the documentation of
the sources via ocamldoc.
This classification attempt could probably be improved. For instance,
the install rules for coqide are currently in Makefile.ide, but could
also go in Makefile.install. Note that I've removed install-library-light
which was broken anyway (arith isn't self-contained anymore).
|
| | | | | |
|
| |/ / /
| | |
| | |
| | |
| | |
| | | |
More precisely, we first remove *.native, *.cm*, *.o, which should
normally consistute the only content of these .coq-native directories,
and then remove these directories if they're indeed empty
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
It has been accidentaly broken since early 2014 (and especially
in 8.5), no easy repair, I won't devote any more hours to this stuff.
Moreover no one seems to care apart from Emilio, but he's ok to work
on this in a separate repository or branch.
I left a dev/doc/ocamlbuild.txt file with a few words about this
experiment.
|
| | | | |
|
| |\ \ \ |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
We delay the externalization of application arguments in Constrextern,
so that they only get computed when they are actually explicitly displayed.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The COQLIBS variable contains some -Q and -I options, which are not
supported by the checker. So this commit introduces a COQCHKLIBS variable
that contains the proper options for coqchk. For the sake of homogeneity,
the COQDOCLIBS variable is also preprocessed in the same way. This means
that both variables have the same value, but they are kept separate in
case the user would like to override one and not the other.
This commit also removes some deprecated options from "coqchk --help".
They are not removed from coqchk itself to preserve backward compatibility
in the branch.
An open question is whether coqchk should support dummy options such as -Q
(interpreted as -R) or -I (ignored).
|
| |\ \ \ \ |
|
| | |\ \ \ \ |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This purely cosmetic effect is obtained by the same variables
$(SHOW) and $(HIDE) as in the main Makefile of Coq.
If you prefer the earlier raw output : make VERBOSE=1
|
| | |/ / / /
| | | | |
| | | | |
| | | | |
| | | | | |
Without this, dependencies upon a .ml4 (or a .mlpack) won't be handled
correctly.
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| |/ / / / |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | | |
and global for 8.4 and 8.5.
|
| | | | | |
|
| |\ \ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Tactic Notation "f" constr(x) := apply x. Ltac g x := f x.
Goal False.
g I. (* Was printing Top.Top#<>#1 *)
idtac; f I. (* Was not properly locating error *)
This is a "a minima" fix.
This a different fix than in trunk, so the merge will have to take the
trunk version.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
An Ltac trace printing mechanism was introduced in 8.4 which was
inadvertedly modified by a series of commits such as 8e10368c3,
91f44f1da7a, ...
It was also sometimes buggy, iirc, when entering ML tactics which
themselves were calling ltac code.
It got really bad in 8.5 as in:
Tactic Notation "f" constr(x) := apply x. Ltac g x := f x.
Goal False.
idtac; f I. (* bad location reporting *)
g I. (* was referring to tactic name "Top.Top#<>#1" *)
which this commit fixes.
I don't have a clear idea of what would be the best ltac tracing
mechanism, but to avoid it to be broken without being noticed, I
started to add some tests.
Eventually, it might be worth that an Ltac expert brainstrom on it!
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| |\ \ \ \ \ |
|
| |/ / / / / |
|
| |\ \ \ \ \ |
|
| | | | | | | |
|
Matthieu Sozeau
Pierre-Marie Pédrot
Hugo Herbelin
Guillaume Melquiond
Jason Gross
Pierre Letouzey
Matej Kosik
Maxime Dénès
Enrico Tassi