| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
The ARGUMENT EXTEND macro was discriminating between parsing entries known
statically, i.e. defined in Pcoq and unknown entires. Although simplifying
a bit the life of the plugin writer, it made actual interpretation difficult
to predict and complicated the code of the ARGUMENT EXTEND macro.
After this patch, all parsing entries and generic arguments used in an
ARGUMENT EXTEND macro must be reachable by the ML code. This requires adding
a few more "open Pcoq.X" and "open Constrarg" here and there.
|
|
|
|
|
|
|
|
It got lost during a merge with the 8.5 branch.
|
|
Try first to find a keyed subterm without conversion/betaiota on open
terms (that is the usual strategy of rewrite), if this fails, try with full
conversion, incuding betaiota. This makes the test-suite pass again,
retaining efficiency in the most common cases.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This is not perfect and repeats what we do in Pcoq, but it is hard to factorize
because rules defined in Pcoq do not have the same precedence. For instance,
constr as a Tactic Notation argument is a Pcoq.Constr.constr while as a
quotation argument is a Pcoq.Constr.lconstr. We should think of a fix in the
long run, but for now it is reasonable to duplicate code.
|
|
|
|
This was redundant with the wit_uconstr generic argument, so there was no real
point on keeping it there.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Checking that a term was indeed a relation was made too early, as the
decomposition function recognized relations of the form "f (g .. (h x y))
with f, g unary and only h binary. We postpone this check to the very end.
|
|
|
|
|
|
This was historically used together with the <:tactic< ... >> quotation to insert
foreign code as $foo, but it actually only survived in the implementation of Tauto.
With the removal of the quotation feature, this is now totally obsolete.
|
|
It used to allow to represent parts of tactic AST directly in ML code. Most of
the uses were trivial, only calling a constant, except for tauto that had an
important code base written in this style. Removing this reduces the dependency
to CAMLPX and the preeminence of Ltac in ML code.
|
|
|
|
unification.
|
|
This gets rid of brittle code written in ML files through Ltac quotations, and
reduces the dependance of Coq to such a feature. This also fixes the particular
instance of bug #2800, although the underlying issue is still there.
|
|
The glob_expr was actually always embedded as a VFun, so this patch should
not change anything semantically. The only change occurs in the plugin API
where one should use the Tacinterp.tactic_of_value function instead of
Tacinterp.eval_tactic.
Moreover, this patch allows to use tactics returning arguments from the ML
side.
|
|
|
|
reflexivity/symmetry/transitivity only need
RelationClasses to be loaded.
|
|
|
|
The setoid_rewrite tactic was not checking that the relation it was looking for
was indeed a relation, i.e. that its type was an arity.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Some functions were left in the old paradigm because they are only used by the
unification algorithms, so they are not worthwhile to change for now.
|
|
Originally, rel-context was represented as:
Context.rel_context = Names.Name.t * Constr.t option * Constr.t
Now it is represented as:
Context.Rel.t = LocalAssum of Names.Name.t * Constr.t
| LocalDef of Names.Name.t * Constr.t * Constr.t
Originally, named-context was represented as:
Context.named_context = Names.Id.t * Constr.t option * Constr.t
Now it is represented as:
Context.Named.t = LocalAssum of Names.Id.t * Constr.t
| LocalDef of Names.Id.t * Constr.t * Constr.t
Motivation:
(1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction"
function which looked like this:
let test_strict_disjunction n lc =
Array.for_all_i (fun i c ->
match (prod_assum (snd (decompose_prod_n_assum n c))) with
| [_,None,c] -> isRel c && Int.equal (destRel c) (n - i)
| _ -> false) 0 lc
Suppose that you do not know about rel-context and named-context.
(that is the case of people who just started to read the source code)
Merlin would tell you that the type of the value you are destructing
by "match" is:
'a * 'b option * Constr.t (* worst-case scenario *)
or
Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *)
To me, this is akin to wearing an opaque veil.
It is hard to figure out the meaning of the values you are looking at.
In particular, it is hard to discover the connection between the value
we are destructing above and the datatypes and functions defined
in the "kernel/context.ml" file.
In this case, the connection is there, but it is not visible
(between the function above and the "Context" module).
------------------------------------------------------------------------
Now consider, what happens when the reader see the same function
presented in the following form:
let test_strict_disjunction n lc =
Array.for_all_i (fun i c ->
match (prod_assum (snd (decompose_prod_n_assum n c))) with
| [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i)
| _ -> false) 0 lc
If the reader haven't seen "LocalAssum" before, (s)he can use Merlin
to jump to the corresponding definition and learn more.
In this case, the connection is there, and it is directly visible
(between the function above and the "Context" module).
(2) Also, if we already have the concepts such as:
- local declaration
- local assumption
- local definition
and we describe these notions meticulously in the Reference Manual,
then it is a real pity not to reinforce the connection
of the actual code with the abstract description we published.
|
