| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
We simply handle the "break" in error messages. Not sure it is the
proper bugfix though, we may want to be able to add breaks in such
recursive notations.
|
|
|
|
variables and definitions in sections is unsupported.
|
|
|
|
Fixpoint/Definition.
|
|
(let x := t in u) a that should be reduced. Maybe a different
decomposition/reduction primitive should be used instead.
|
|
It was not detected because of a "bug" in clear checking the existence
of the hypothesis only at interpretation time (not at execution time).
|
|
(e.g. with deprecated options such as -byte, etc.) since I guess this
is what we expect.
Was probably lost in 81eb133d64ac81cb.
|
|
- Fixing dead code, doc.
- Relaxing constraints on using an as-tuple in inversion.
|
|
|
|
|
|
The length of the pattern should now be exactly the number of
assumptions and definitions introduced by the destruction or induction,
including the induction hypotheses in case of an induction.
Like for pattern-matching, the local definitions in the argument of
the constructor can be skipped in which case a name is automatically
created for these.
|
|
Basically, the hypotheses were treated in an incorrect order, with a
hack for sometimes put them again in the right order, resulting in
failures and redundant hypotheses.
Status unclear, because this new version is incompatible except in
simple cases like a double induction on two "nat".
Fixing the bug incidentally simplify the code, relying on the
deprecation since 8.4 to allow not to ensure a compatibility (beyond
the simple situation of a double induction on simple datatypes).
See file induct.v for effect of changes.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This is useful for restoring bullets after e.g. loading ssreflect.
Hoping Arnaud is ok in documenting it.
|
|
Following a discussion on coq-club on Jan 13, 2016.
|
|
|
|
|
|
|
