| Commit message (Collapse) | Author | Age |
|
|
|
| |
observe non-normalized goals.
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
The removed code isn't used locally and isn't exported in the signature
|
|
|
|
|
|
|
|
| |
With ocaml 4.01, the 'unused open' warning also checks the mli :-)
Beware: some open are reported as useless when compiling with camlp5,
but are necessary for compatibility with camlp4. These open are now
marked with a comment.
|
|
|
|
|
|
| |
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.
|
|
|
|
|
| |
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
|
| |
|
| |
|
| |
|
|
|
| |
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.
|
| |
|
|
|
| |
It fixes micromega. It is frankly a mystery to me why psatz ever work. The semantics of Ltac's match is still fishy.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
I'm trying to avoid unecessary construction of intermediate lists. Interpretation function don't modify the goals, they just need a goal in their
context.
Some care has to be given to the evar maps, though, as we can extract an outdated evar map from a goal (this is probably an undesirable feature, but significantly simplified the compatibility API).
Also, Proofview.Goal.enter{,l} catch exceptions (and transfer the non-critical ones into errors of the tactics monad). So I had to do just that for every "enter" removed (I probably have been overprotective but it's better that way).
Not as trivial a modification as it should, but it will hopefully go over well. It was much needed anyway.
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
| |
View types are better practice than option types for pattern-matching. (Plus, they save a minute amount of allocations)
|
|
|
|
|
|
|
|
|
|
| |
containing opaque grammar objects, it now contains a string representing
the entry. In order to recover the entry from the string, the former must
have been created with [Pcoq.create_generic_entry] or similar. This is
guaranteed for entries generated by ARGUMENT EXTEND, and must be done by
hand otherwise.
Some plugins were fixed accordingly.
|
| |
|
| |
|
|
|
|
| |
Following a remark by Jason Gross and Daniel Grayson.
|
|
|
|
| |
monad.
|
| |
|
|
|
|
| |
hypothesis.
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
| |
To make this possible the state id has to reach the kernel.
Hence definition_entry has an extra field, and many files had
to be fixed.
|
| |
|
| |
|