| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | | |
|
| | |
| |
| |
| |
| | |
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.
|
| | | | |
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| | |
multiple patterns.
|
| | |
| |
| |
| |
| | |
Instead of relying on a costly set union, we take advantage of the fact
that instances are small compared to the set of universes.
|
| | | |
|
| | |
| |
| |
| |
| | |
It is similar to find but raises an assertion failure instead of a Not_found
when the element is not encountered. Using it will give stronger invariants.
|
| | | |
|
| | |
| |
| |
| | |
This patch was proposed by JH in bug report #4547.
|
| | | |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| | |
The performance enhancement introduced by a895b2c0 for non-polymorphic hints
was actually causing a huge regression in the polymorphic case (and was marked
as such). We fix this by only substituting the metas from the evarmap instead
of the whole evarmap.
|
| | |
| |
| |
| |
| |
| |
| |
| | |
For instance, in
Inductive I : nat -> nat -> Prop := C : forall z, let '(x,y) := z in x + y = 0.
the computation of the number of arguments to I was made wrong in bde12b70.
|
| | | |
|
| | | |
|
| | | |
|
Pierre-Marie Pédrot
Matthieu Sozeau
Enrico Tassi
Matej Kosik
Pierre Letouzey
Emilio Jesus Gallego Arias
Hugo Herbelin