| Age | Commit message (Collapse) | Author |
|---|
|
duplicates in kernel side effects. They were chosen according to an equality
that was quite irrelevant, and as expected this patch did not break the
test-suite.
|
|
|
|
|
|
|
|
|
|
|
|
file was useless and duplicated code from Btermdn itself.
|
|
|
|
|
|
|
|
There are currently two other clashs : Lexer and Errors, but for
the moment these ones haven't impacted my experiments with extraction
and compiler-libs, while this Matching issue had. And anyway the new
name is more descriptive, in the spirit of the recent TacticMatching.
|
|
Anyway, a few syntactic features of 3.12 were already used here and
there (e.g. local opening via Foo.(...), or the record shortcut
{ field; ... }). Hence compiling with 3.11 wasn't working anymore.
Already take advantage of the following 3.12.1 features :
- "module type of ..." in CArray, CList, CString ...
- "ocamldep -ml-synonym" : no need anymore to hack the ocamldep output
via our coqdep to localize the .ml4 modules :-)
The -ml-synonym option (+ various bugfixes) is the reason for asking
3.12.1 directly and not just 3.12.0. After all, if debian stable is
providing 3.12.1, then everybody has it ;-)
|
|
In last commit, we used grep to decide whether a .ml4 could be
compiled during the initial phase of not. Instead, we now rely on
a simpler directory dichotomy:
- config lib kernel library pretyping interp parsing grammar
are considered initial (and shouldn't contain grammar-dependent .ml4),
see $(GRAMSRCDIRS) in Makefile.common
- the grammar-dependent .ml4 could be in any other directories
Currently, they are in: tactics toplevel plugins/*
|
|
This almost reverts commit 845d6f (r15248).
It isn't ideal to put syntactic stuff in the toplevel directory.
Maybe this kind of files should have someday their own directory
along with g_rewrite.ml4 and some other (maybe a extraparsing dir?).
Meanwhile, this commit leads to a cleaner situation concerning *.ml4:
- everything needed to build grammar.cma (and q_constr.cmo) is in:
lib/ kernel/ library/ pretyping/ interp/ proofs/ parsing/ grammar/
- all *.ml4 using grammar.cma (or q_constr.cmo) are in:
tactics/ toplevel/ plugins/*/
|
|
NB: new file miscprint.ml deserves to be part of printing.cma,
but should be part of proofs.cma for the moment, due to use in logic.ml
|
|
|
|
|
|
|
|
|
|
|
|
|
|
reserved with Implicit Type.
|
|
|
|
|
|
optimization purposes. I replaced their use with the under-approximation
of pointer equality.
|
|
|
|
|
|
|
|
Helps cbn tactic refolding
|
|
infinite loop.
|
|
|
|
|
|
|
|
|
|
|
|
Problems:
- strip may not be "strip" but "i686-bla-strip", hence we ask ocamlc -config
the value of "ranlinb" and replace ranlib by strip obtaining
"i686-bla-strip" from "i686-bla-ranlib"
- coq_makefile was not quoting the plugins/ paths
- coq_makefile was quoting twice camlpX (the shell of cygwin was confused)
|
|
|
|
Yet another revision of the build system. We avoid relying on the awkward
include-which-fails-but-works-finally-after-a-retry feature of gnu make.
This was working, but was quite hard to understand. Instead, we reuse
the idea of two explicit phases (as in 2007 and its stage{1,2,3}), but
in a lighter way. The main Makefile calls Makefile.build twice :
- first for building grammar.cma (and q_constr.cmo), with a restricted
set of .ml4 to consider (see variables BUILDGRAMMAR and ML4BASEFILES).
- then on the true target(s) asked by the user (using the special variable
MAKECMDGOALS).
In pratice, this should change very little to the concrete developper's life,
let me know otherwise. A few more messages of make due to the explicit
first sub-call, but no more strange "not ready yet" messages...
Btw: we should handle correctly now the parallel compilation of multiple
targets (e.g. make -jX foo bar). As reported by Pierre B, this was
triggering earlier two separate sub-calls to Makefile.build, one
for foo, the other for bar, with possibly nasty interactions in case
of parallelism.
In addition, some cleanup of Makefile.build, removal of useless :: rules,
etc etc.
|
|
|
|
|
|
Introducing List.fold_right and List.fold_left in Monad.
|
|
Adds a combinator List.map_right which chains effects from right to left.
|
|
|
|
This commit also introduces a module Monad to generate monadic combinators (currently, only List.map).
|
|
Impacts MapleMode.
|
|
The prefered style is to use continuation passing style when necessary, or simply passing the goal explicitely in the case of interpretation functions which do not evolve the current goal.
|
|
|
|
This changes the tacinterp API, but only affects (one line of) the MapleMode contrib.
|
|
|
|
|
