index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
/
success
Commit message (
Expand
)
Author
Age
*
Fix files in test-suite having to do with Require inside modules.
Maxime Dénès
2015-01-12
*
Update headers.
Maxime Dénès
2015-01-12
*
Extraction: discard code unnecessary to fulfill a module signature
Pierre Letouzey
2015-01-11
*
An optimization in the use of unification candidates so as to get the
Hugo Herbelin
2015-01-01
*
Better doc and a few fixes for Proof using.
Enrico Tassi
2014-12-19
*
Proof using: New vernacular to name sets of section variables
Enrico Tassi
2014-12-18
*
fix bug #2447 in congruence
Pierre Corbineau
2014-12-16
*
Fixing orientation of postponed subtyping problems.
Hugo Herbelin
2014-12-10
*
Improving evar restriction (this is a risky change, as I remember a
Hugo Herbelin
2014-12-07
*
Take benefit of improved name preservation of evars in e2fa65fcc.
Hugo Herbelin
2014-12-04
*
When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' if
Hugo Herbelin
2014-12-02
*
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-25
*
Add test-suite file for dependent rewriting example by Vadim Zaliva and
Matthieu Sozeau
2014-11-22
*
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-18
*
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-16
*
Preserving the good effect of 014e5ac92a on not leaving dangling local
Hugo Herbelin
2014-11-14
*
Removing yet another source of remaining local definitions.
Hugo Herbelin
2014-11-13
*
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-08
*
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-06
*
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-03
*
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-11-02
*
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-31
*
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-27
*
Fixing destruct/induction with a using clause on a non-inductive type,
Hugo Herbelin
2014-10-26
*
This commit introduces changes in induction and destruct.
Hugo Herbelin
2014-10-25
*
Fixing an evar leak in pattern-matching compilation (#3758).
Hugo Herbelin
2014-10-22
*
Fixing a bug in the presence of let-in in inductive arity.
Hugo Herbelin
2014-10-20
*
Relaxing again the test on types of replacements in tactic change
Hugo Herbelin
2014-10-16
*
Added support for several impossible cases in compilation of "match".
Hugo Herbelin
2014-10-13
*
A few improvements on pattern-matching compilation.
Hugo Herbelin
2014-10-05
*
Seeing IntroWildcard as an action intro pattern rather than as a naming pattern
Hugo Herbelin
2014-09-30
*
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-29
*
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-27
*
Fixing #3641 (loop in e_contextually, introduced in r16525).
Hugo Herbelin
2014-09-19
*
Update test-suite files after last commit. Add a file for rewrite_strat
Matthieu Sozeau
2014-09-17
[next]