| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Making a clear distinction between expressions of the notation which
are associated to binding variables only (as in `Notation "'lam' x ,
P" := (fun x => P)" or `Notation "'exists2' x : t , p & q" := (ex2
(fun x:t => p) (fun x:t => q))') and those which are associated to
at list one subterm (e.g. `Notation "x .+1" := (S x)' but also
"Notation "{# x | P }" := (ex2 _ (fun y => x = F y) (fun x => P))'
as in #4592). The former have type NtnTypeOnlyBinder.
- Thus avoiding in particular encoding too early Anonymous as GHole
and "Name id" as "GVar id".
There is a non-trivial alpha-conversion work to do to get #4592
working. See comments in Notation_ops.add_env.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
| |
File contributed by Cédric Auger (a long time ago, sorry!)
Qarith and Qc would probably deserve many more results like this one,
and a more modern style (for instance qualified names), but this commit
is better than nothing...
|
| | |
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| |
| |
| | |
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 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.
|
| |/
|
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
|
|
| |
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.
|
| |\ \ |
|
| | | | |
|
| |/ / |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Print and Extraction commands may pierce opacity: if the
task producing the proof term is not finished, we wait for
its completion.
In -quick mode no worker is going to process a task, since tasks
are simply stored to disk (and resumed later in -vio2vo mode).
This commit avoids coqc waits forever for a task in order to
Print/Extract the corresponding term. Bug reported privately
by Alec Faithfull.
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
"Instance name : Type." is like "Lemma name : Type", i.e. it starts
a proof. Unfortunately sometimes it does not, so we say VtUnknown.
Still, if there is an open proof, we classify it as a regular Lemma,
i.e. the opacity depends only on the terminator.
This makes CoqIDE and PIDE based UI way more responsive when processing
files containing Instance that are proved by tactics, since they are now
correctly delegated to workers. Bug reported privately by Alec Faithfull.
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Two new (trivial) functions were added:
Names.Name.is_anonymous : Names.Name.t -> bool
Names.Name.is_name : Names.Name.t -> bool
They enable us to write a more compact code.
(example: commit "99633f4" in "relation-extraction" module of "coq-contribs").
|
| | |
| |
| |
| |
| | |
The environment put in the goals was not the right one and could lead to
various leaks.
|
| | |
| |
| |
| |
| | |
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.
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
I propose to change the name of the "Util.compose" function to "%".
Reasons:
1. If one wants to express function composition,
then the new name enables us to achieve this goal easier.
2. In "Batteries Included" they had made the same choice.
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The original datatype:
Entries.local_entry = LocalDef of constr
| LocalAssum of constr
was changed to:
Entries.local_entry = LocalDefEntry of constr
| LocalAssumEntry of constr
There are two advantages:
1. the new names are consistent with other variant names in the same module
which also have this "*Entry" suffix
2. the new names do not collide with variants defined in the Context.{Rel,Named}.Declaration
modules so both, "Entries" as well as "Context.{Rel,Named}.Declaration" can be open at the same time.
The disadvantage is that those new variants are longer.
But since those variants are rarely used, it it is not a big deal.
|
| | | | |
|
| |/| | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
...
...
...
...
...
...
...
...
...
...
...
...
...
...
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | | |
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.
|
| |\ \ \
| | |/
| |/| |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The current solution may not be totally ideal though. We generate names for
anonymous evars on the fly at printing time, based on the Evar_kind data they
are wearing. This means in particular that the printed name of an anonymous
evar may change in the future because some unrelate evar has been solved or
introduced.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
It used not to be the case when the proof contains Sideff, since
the code was picking the last known state and not necessarily the
first one. Because of side effects the last known state could be
the one corresponding to the side effect (that was executed to, say,
change the parser). This is also related to bug #4530
|
| | | | |
|
| | | |
| | |
| | |
| | | |
This fixes micromega in certain environments.
|
| | | | |
|
Hugo Herbelin
Pierre-Marie Pédrot
Pierre Letouzey
Matthieu Sozeau
Enrico Tassi
Matej Kosik
Emilio Jesus Gallego Arias