| Age | Commit message (Collapse) | Author |
|
We're back to a unique build phase (as before e372b72), but without
relying on the awkward include-deps-failed-lets-retry feature of make.
Since PMP has made grammar/ self-contained, we could now build
grammar.cma in a rather straightforward way, no need for
a specific sub-call to $(MAKE) for that. The dependencies between
files of grammar/ are stated explicitely, since .d files aren't
fully available initially.
Some Makefile simplifications, for instance remove the CAMLP4DEPS
shell horror. Instead, we generalize the use of two different
filename extensions :
- a .mlp do not need grammar.cma (they are in grammar/ and tools/compat5*.mlp)
- a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo),
except coqide_main.ml4 and its specific rule
Note that we do not generate .ml4.d anymore (thanks to the .mlp vs.
.ml4 dichotomy)
|
|
|
|
Since TACTIC EXTEND relies on the usual tactic notation mechanism, the
interpretation of an ML tactic first goes through a TacAlias node. This
means that variables bound by the notation overwrite those of the current
environment. It turns out to be problematic for badly designed arguments
that close over variables of the environment, e.g. glob_constr, because
the variables used at interpretation time are now different from the ones
of parsing time.
Ideally, those arguments should return a closure made of the inner argument
together with the Ltac environment they were defined in. Unluckily, this would
need some important changes in their design. Most notably, most of ssreflect
ARGUMENT EXTEND actually create such closed arguments.
In order to emulate the old behaviour, we rather use a hack by prefixing
ML-bound variables by a character that is not accessible from user-side.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This fixes parsing conflicts with the [fix ... with] tactic.
|
|
This makes the TACTIC EXTEND macro insensitive to Coq-defined arguments. They
now have to be reachable in the ML code. Note that this has some consequences,
as the previous macro was potentially mixing grammar entries and arguments as
long as their name was the same. Now, each genarg comes with its grammar
instead, so there is no way to abuse the macro.
|
|
|
|
It implemented the quotation logic of terms and tactics, although it was
mostly obsolete. With quotations gone, it is now useless and thus removed.
I fundamentally doubt that anyone hardly depends on this out there.
|
|
|
|
|
|
|
|
|
|
|
|
Actually the identifier was never used and just carried along.
|
|
|
|
|
|
|
|
|
|
|
|
Entries defined in the Pcoq AST of symbols must be marshallable, because they
are present in the libstack. Yet, CAMLP4/5 entries are not marshallable as
they contain functional values. This is why the Pcoq module used a pair
[string * string] to describe entries. It is obviously type-unsafe, so
we define a new abstract type in its own module. There is a little issue
though, which is that our entries and CAMLP4/5 entries must be kept
synchronized through an association table. The Pcoq module tries to
maintain this invariant.
|
|
|
|
|
|
|
|
Conflicts:
tactics/eauto.ml4
(merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)
|
|
TACTIC EXTEND (based on user-given name).
|
|
Now that ML tactics are not dispatched according to the type of their arguments
anymore, one has to take care of the way potentially atomic tactics are handled.
This patch ensures that the atomic tactics generated by the TACTIC EXTEND
macro have the right length and the right order.
There may be very rare trouble if two ML tactics in the same entry are of the
form
"foo" x1 ... xn
"foo" y1 ... ym
where all xi and yi may be empty. I doubt that the legacy implementation
behaved well in this case anyway.
|
|
Furthermore, ML tactic dispatch is not done according to the
type of its argument anymore.
|
|
This will allow to get rid of the fragile mechanism of discriminating which
entry to call depending on the dynamic type of its arguments.
|
|
|
|
|
|
- Do use the flag for_ml for distinguishing coq level and ml level
ltac definitions.
- Skip ML call from the trace.
There are still differences from 8.4 and trunk. For instance on:
Ltac f x := refine x.
Goal False.
f I.
8.4 says:
In nested Ltac calls to "f" and "x" (with x:=I), last term evaluation failed.
Error: The term "I" has type "True" while it is expected to have type "False".
trunk says:
In nested Ltac calls to "f" and "refine <genarg:uconstr>", last call failed.
Error: The term "I" has type "True" while it is expected to have type "False".
Maybe we would like a mix of both (besides the printing of a
non-elegant "<genarg:uconstr>)?
|
|
1. Proofview.Goal.enter into Proofview.Goal.nf_enter.
2. Proofview.Goal.raw_enter into Proofview.Goal.enter.
3. Proofview.Goal.goals -> Proofview.Goals.nf_goals
4. Proofview.Goal.raw_goals -> Proofview.Goals.goals
5. Ftactic.goals -> Ftactic.nf_goals
6. Ftactic.raw_goals -> Ftactic.goals
This is more uniform with the other functions of Coq.
|
|
This allows to directly register globtactics in the Tacenv API, without
having to resort to any internalization function.
|
|
Also taking advantage of the change to rename it into TacML. Ultimately
should allow ML tactic to return values.
|
|
potentially conflicting tactics names from different plugins.
|
|
proof. Indeed, computing an empty list of arguments triggered a
Proofview.Goal.enter, which broke tactics like [shelve_unifiable].
This does not fix this particular tactic though, because the Ltac
interpreter still enters the goal when calling a Ltac reference.
|
|
"foobar" constr(x1) ... constr(xn)
are now defined as pure Ltac definitions, and do not add grammar
nor printing rules. This partially relies on a hack consisting
in retrieving the arguments in the tactic environment rather than
as directly passed to the TacExtend node.
|
|
|
|
not create grammar and printing rules anymore, they define Ltac entries
in the module that declares them instead.
|
|
corresponding Declare ML Module command. This changes essentially two
things:
1. ML plugins are forced to use the DECLARE PLUGIN statement before any
TACTIC EXTEND statement. The plugin name must be exactly the string passed to
the Declare ML Module command.
2. ML tactics are only made available after the Coq module that does the
corresponding Declare ML Module is imported. This may break a few things,
as it already broke quite some uses of omega in the stdlib.
|
|
|
|
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.
|
|
they never produce a VernacExtend entry.
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17080 85f007b7-540e-0410-9357-904b9bb8a0f7
|