| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
(but deactivated still).
Set Keyed Unification to activate the option, which changes
subterm selection to _always_ use full conversion _after_ finding a
subterm whose head/key matches the key of the term we're looking for.
This applies to rewrite and higher-order unification in
apply/elim/destruct.
Most proof scripts already abide by these semantics. For those that
don't, it's usually only a matter of using:
Declare Equivalent Keys f g.
This make keyed unification consider f and g to match as keys.
This takes care of most cases of abbreviations: typically Def foo :=
bar and rewriting with a bar-headed lhs in a goal mentioning foo works
once they're set equivalent.
For canonical structures, these hints should be automatically declared.
For non-global-reference headed terms, the key is the constructor name
(Sort, Prod...). Evars and metas are no keys.
INCOMPATIBILITIES:
In FMapFullAVL, a Function definition doesn't go through with keyed
unification on.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
avoid looping and be compatible with unfold.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
for primitive projections, fixing bug #3661. Also fix expand_projection
so that it does enough reduction to find the inductive type of its
argument.
|
| |
|
|
|
|
|
|
| |
so as to reproduce correctly the reduction behavior of existing
projections, i.e. delta + iota. Make [projection] an abstract datatype
in Names.ml, most of the patch is about using that abstraction.
Fix unification.ml which tried canonical projections too early in
presence of primitive projections.
|
Matthieu Sozeau
Pierre Boutillier
Hugo Herbelin
Carst Tankink
Enrico Tassi
Pierre-Marie Pédrot
Xavier Clerc