index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test-suite
/
success
Age
Commit message (
Expand
)
Author
2015-01-01
An optimization in the use of unification candidates so as to get the
Hugo Herbelin
2014-12-19
Better doc and a few fixes for Proof using.
Enrico Tassi
2014-12-18
Proof using: New vernacular to name sets of section variables
Enrico Tassi
2014-12-16
fix bug #2447 in congruence
Pierre Corbineau
2014-12-10
Fixing orientation of postponed subtyping problems.
Hugo Herbelin
2014-12-07
Improving evar restriction (this is a risky change, as I remember a
Hugo Herbelin
2014-12-04
Take benefit of improved name preservation of evars in e2fa65fcc.
Hugo Herbelin
2014-12-02
When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' if
Hugo Herbelin
2014-11-25
Adapting to current semantics of "simpl non-evaluable-cst"
Hugo Herbelin
2014-11-25
Experimenting using unification when matching evar/meta free subterms
Hugo Herbelin
2014-11-22
Add test-suite file for dependent rewriting example by Vadim Zaliva and
Matthieu Sozeau
2014-11-18
Fixing a little bug with nested but convertible occurrences in "destruct at".
Hugo Herbelin
2014-11-18
Fixing detection of occurrences in the presence of nested subterms for
Hugo Herbelin
2014-11-16
Enforcing a stronger difference between the two syntaxes "simpl
Hugo Herbelin
2014-11-16
Fixing side bug in db37c9f3f32ae7 delaying interpretation of the
Hugo Herbelin
2014-11-14
Preserving the good effect of 014e5ac92a on not leaving dangling local
Hugo Herbelin
2014-11-13
Removing yet another source of remaining local definitions.
Hugo Herbelin
2014-11-08
Follow up to experimental eager evar unification in bcba6d1bc9:
Hugo Herbelin
2014-11-08
Compatibility with 8.4 in the heuristic used to build the induction
Hugo Herbelin
2014-11-06
Restoring clear_flag (thanks a lot to jonikelee to notice it).
Hugo Herbelin
2014-11-06
Optimizing when to clear generalized hypotheses in destruct.
Hugo Herbelin
2014-11-06
Removing "destruct" test not yet working.
Hugo Herbelin
2014-11-03
Subtle swap of lines to preserve VarInstance src field before checking
Hugo Herbelin
2014-11-03
Fix to 844431761 on improving elimination with indices, getting rid of
Hugo Herbelin
2014-11-02
Improving elimination with indices, getting rid of intrusive residual
Hugo Herbelin
2014-11-02
Some reorganization of the code for destruct/induction:
Hugo Herbelin
2014-11-02
Fixing file destruct.v.
Hugo Herbelin
2014-10-31
Enlarge the cases where the like first selection is used in destruct.
Hugo Herbelin
2014-10-31
Listing a few examples of destruct showing unsatisfactory behaviors.
Hugo Herbelin
2014-10-31
Avoid "destruct H" to apply on H itself when H is a section variable.
Hugo Herbelin
2014-10-27
Making destruct on idents with maximal implicit arguments working, by
Hugo Herbelin
2014-10-27
Ensuring compatibility when an hypothesis used for destruct is
Hugo Herbelin
2014-10-27
Fixing clash in test destruct.v.
Hugo Herbelin
2014-10-26
Fixing destruct/induction with a using clause on a non-inductive type,
Hugo Herbelin
2014-10-25
This commit introduces changes in induction and destruct.
Hugo Herbelin
2014-10-22
Fixing an evar leak in pattern-matching compilation (#3758).
Hugo Herbelin
2014-10-20
Fixing a bug in the presence of let-in in inductive arity.
Hugo Herbelin
2014-10-16
Relaxing again the test on types of replacements in tactic change
Hugo Herbelin
2014-10-13
Added support for several impossible cases in compilation of "match".
Hugo Herbelin
2014-10-05
A few improvements on pattern-matching compilation.
Hugo Herbelin
2014-09-30
Seeing IntroWildcard as an action intro pattern rather than as a naming pattern
Hugo Herbelin
2014-09-29
Restoring non-uniform delta on local and global constants in 2nd order
Hugo Herbelin
2014-09-29
Fix test-suite files
Matthieu Sozeau
2014-09-27
Keyed unification option, compiling the whole standard library
Matthieu Sozeau
2014-09-27
First version of keyed subterm selection in unification.
Matthieu Sozeau
2014-09-19
Fixing #3641 (loop in e_contextually, introduced in r16525).
Hugo Herbelin
2014-09-17
Update test-suite files after last commit. Add a file for rewrite_strat
Matthieu Sozeau
2014-09-17
Revert specific syntax for primitive projections, avoiding ugly
Matthieu Sozeau
2014-09-16
fix test-suite/success/decl_mode.v
Enrico Tassi
2014-09-15
Add a "Hint Mode ref (+ | -)*" hint for setting a global mode
Matthieu Sozeau
[next]
