| Commit message (Collapse) | Author | Age |
... | |
| |
| |
| |
| |
| |
| |
| | |
The ARGUMENT EXTEND statement was wrongly using a CompatLoc instead of a Loc,
and this was not detected by typing "thanks" to the Gram.action magic. When
using CAMLP4, this was wreaking havoc at runtime, but not when using CAMLP5,
as the locations where sharing the same representation.
|
| |
| |
| |
| |
| | |
Amongs other things, it kind of fixes bug #4492, even though you cannot really
take advantage of the parsed data for now.
|
| |
| |
| |
| |
| |
| | |
METAIDENT were idents of the form $foobar, only used in quotations.
Note that it removes two dollars in the Coq codebase! Guess I'm absolved
for the $(...) syntax.
|
| |
| |
| |
| |
| |
| | |
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.
|
| | |
|
|\| |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
|\|
| |
| |
| |
| | |
Conflicts:
lib/cSig.mli
|
| |
| |
| |
| |
| |
| |
| |
| | |
CString was linked after Serialize, although the later was using CString.equal.
This had not been noticed so far because OCaml was ignoring functions marked as
external in interfaces (which is the case of CString.equal) when considering
link dependencies. This was changed on the OCaml side as part of the fix of
PR#6956, so linking was now failing in several places.
|
| |
| |
| |
| | |
Actually the identifier was never used and just carried along.
|
| | |
|
| |
| |
| |
| |
| |
| |
| | |
Kind of enhances the situation of bug #4409. Now arguments can be interpreted
globally or focussedly in a dynamic fashion because the interpretation function
returns a Ftactic.t. The bug is not fixed yet because we should tweak the
interpretation of tactic arguments.
|
| |
| |
| |
| |
| | |
We also intepret it at toplevel as a true constr and push the resulting
evarmap in the current state.
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| | |
Now that types can share the same dynamic representation, we do not have
to transtype the topelvel values dynamically and just take advantage of
the standard interpretation function.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
|
| | |
|
| | |
|
|\| |
|
| | |
|
| |
| |
| |
| | |
This allows fatal_error to be used for printing anomalies at loading time.
|
| |
| |
| |
| | |
This allows fatal_error to be used for printing anomalies at loading time.
|
|\|
| |
| |
| |
| |
| |
| | |
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.
|
| |
|
|
|
|
|
|
| |
there is no focused goal.
The 'g' is for "global". The arguments are the same as [fail]. Beware: [let x := constr:… in tac] is a goal-local operation regardless of whether [tac] is goal-local or not.
|
|
|
|
|
|
| |
This was due to the unqualified uses of "Lazy" being disambiguated in different manners. I just changed the constructor name to "Select".
Fixes #3877.
|