| Age | Commit message (Collapse) | Author |
|---|
|
|
|
inductives).
The implementation constant should have the a universe instance
of the same length, we assume the universes are in the same order
and we check that the definition does not add any constraints
to the expected ones. This fixes bug #3670.
|
|
it became possible to have binding names themselves bound to ltac
variables (2fcc458af16b).
|
|
|
|
glob_constr to constr_pattern. Was partially fixed to solve #3088
(8e88b7adab) in but the order of lambdas was still incorrect as the
fix of the order of lambdas in second-order pattern-matching for #3136
showed (83159124ce22).
|
|
|
|
- unbound variables in notation are allowed, forcing only parsing mode
- plus and mult are now themselves abbreviations
- evars are named
|
|
|
|
This reverts commit cc06ffe3df0ecc023ad046a085b0751ed4161cbf.
Going back to the convention of naming bound variables in hypotheses
of the goal as in 8.4.
My arguments for the revert are:
- apply ... with (id:=...) would have to be changed too, then possibly
breaking the compatibility
- the naming became dependent of the order of variables as in
x:nat
H:forall x0, x0=0
=====
goal
but
H:forall x, x=0
x:nat
=====
goal
Accordingly, this is all a matter of convention, since the meaning of
bindings is anyway the same in both cases.
|
|
constants which without a @ would have a maximally inserted implicit
argument.
|
|
Was just printed in the case of internal holes.
Also: replace [str] by [strbrk] in error message of unsolved holes for better layout.
|
|
potentially different types, resulting in ill-typed terms due to eta.
Projection expansion now fails gracefully on retyping errors.
The proper fix to unification, checking that the heads for FO
have unifiable types, is currently too strong, adding unnecessary universe
constraints, so it is disabled for now. It might be quite expensive
too also it's not noticeable on the stdlib.
|
|
it closer to evarconv/unification's behavior and it is less prone
to weird failures and successes in case of first-order unification
sending problems where the two terms have different types.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
not draw Auto.
|
|
works correctly with an hypothesis of the context and knowing that
related bug #3204 had its own fix.
|
|
by names): VarInstance behaves like GoalEvar for type class
resolution.
|
|
reorganization of apply in d5fece25d8964d5d9fcd55b66164286aeef5fb9f:
using renaming also in retyping.
|
|
|
|
The leafs of the XML trees are still pretty-printed strings, but this
could be refined later on.
|
|
The more structured goal record type of CoqIDE is also useful for other
interfaces (in particular, for PIDE). To support this, the datatype was
factored out to the Proof module. In addition, the record gains a type
parameter, to allow interfaces to adapt the output to their needs.
To accommodate this type, the Proof module also gains the
map_structured_proof that takes a Proof.proof and a function on the
individual goals (in the context of an evar map) and produces a
structured goal based on the goal transformer.
|
|
|
|
These plugins, like coqidetop, stmworkertop and tacworkertop are
intended for toploop replacements (see -toploop command line option).
With this commit coq_makefile can be used as the build system for
any user-interface-specific plugins.
|
|
Naming a Ltac definition like a built-in tactic used to fail, but now only
spits out a warning. This is too complicated to test...
|
|
|
|
|
|
(the action is "clear").
Added subst_intropattern which was missing since the introduction of
ApplyOn intro patterns.
Still to do: make "intros _ ?id" working without interferences when
"id" is precisely the internal name used for hypotheses to discard.
|
|
will name the goal id; writing ?[?id] will use the first
fresh name available based with prefix id.
Tactics intro, rename, change, ... from logic.ml now preserve goal
name; cut preserves goal name on its main premise.
|
|
using whd_state_gen to handle unfolding. Add an isProj/destProj
in term. Use the proper environment everywhere in unification.ml.
|
|
It is not 100% complete, but the main part is there.
|
|
so that one can retrieve them and pass them to third party tools (i.e.
print the AST with the notations attached to the nodes concerned).
Available syntax:
- all in one:
Notation "a /\ b" := ... (format "...", format "latex" "#1 \wedge #2").
- a posteriori:
Format Notation "a /\ b" "latex" "#1 \wedge #2".
|
|
|
|
|
|
|
|
- Removed collect_evars which does not consider instance
(use evars_of_term instead).
- Also removed evars_of_evar_info which did not filter context (use
evars_of_filterered_evar_info instead). This is consistent with
printing goal contexts in the filtered way.
Anyway, as of today, afaics goals filters are trivial
because (if I interpret evarutil.ml correctly), evars with
non-trivial filter necessarily occur in a conv pb. Conversely,
conv pbs being solved when tactics are called, there should not be
an evar used as a goal with a non-trivial filter.
|
|
|
|
unification for apply (compatibility reason). Waiting for another way
to provide a more uniform scheme by default (keyed unification?).
|
|
|
|
|
|
|
|
3566 gave a legitimate error, keyedrewrite was not setting keyed
unification on.
|
|
|
|
their eta-expanded forms which can then unfold back to the unfolded
primitive projection form. This removes all special code that
was necessary to handle primitive projections before, while keeping
compatibility.
Also fix cbn which was not refolding primitive projections correctly
in all cases.
Update some test-suite files accordingly.
|
|
|
