index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
Commit message (
Expand
)
Author
Age
*
First debug... the renaming of librairies was not working and auto/dn were no...
soubiran
2009-10-23
*
This big commit addresses two problems:
soubiran
2009-10-21
*
Fix bug in typeclass resolution discoverd by Eeelis van der Weegen:
msozeau
2009-10-15
*
Relaxed error severity when encountering unknown library objects or tactic
gmelquio
2009-10-06
*
Correctly do backtracking during type class resolution even if only new
msozeau
2009-10-05
*
Changed the way to support compatibility with previous versions.
herbelin
2009-10-04
*
Removal of trailing spaces.
serpyc
2009-10-04
*
Added option "Unset Dependent Propositions Elimination" to protect
herbelin
2009-10-03
*
Remove legacy export_* functions
glondu
2009-09-29
*
Apply "Declare Implicit Tactic" also to terms interpreted as "open
herbelin
2009-09-27
*
Fixed a bug in the interaction between dEqThen and inject_at_positions
herbelin
2009-09-27
*
Delay the choice of eliminator in destruct/induction until we know if
herbelin
2009-09-27
*
Fixed a hole in glob_tactic that allowed some Ltac code to refer to
herbelin
2009-09-26
*
Better use of transparency information for local hypotheses:
msozeau
2009-09-22
*
Only one "in" clause in "destruct" even for a multiple "destruct".
herbelin
2009-09-20
*
- Fixed a bug in checking that implicit arguments are all correctly
herbelin
2009-09-18
*
Remove useless Liboject.export_function field
glondu
2009-09-17
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
- Inductive types in the "using" option of auto/eauto/firstorder are
herbelin
2009-09-13
*
Generalized the possibility to refer to a global name by a notation
herbelin
2009-09-11
*
Added syntax "exists bindings, ..., bindings" for iterated "exists".
herbelin
2009-09-10
*
Allow setoid rewrite to rewrite in pattern-matching scrutinees or
msozeau
2009-09-09
*
Stop trying to search if the relation is declared as a [RewriteRelation]
msozeau
2009-09-09
*
Fix the bug-ridden code used to choose leibniz or generalized
msozeau
2009-09-08
*
Support globality flag properly for "Add Morphism foo : foo_mor" syntax.
msozeau
2009-09-03
*
Stop unnecessary use of lazy values for constraints, simplifying
msozeau
2009-09-02
*
Death of "survive_module" and "survive_section" (the first one was
herbelin
2009-08-13
*
- Cleaning phase of the interfaces of libnames.ml and nametab.ml
herbelin
2009-08-06
*
Move out JMeq of subst for compatibility (it affects e.g. the
herbelin
2009-08-06
*
- Add more precise error localisation when one of the application fails
herbelin
2009-08-04
*
Fixed subst failing when a truly heterogeneous JMeq hyp is in the
herbelin
2009-08-04
*
Added "etransitivity".
herbelin
2009-08-03
*
Improved parameterization of Coq:
herbelin
2009-08-02
*
Fixed a typo in "info" for tactic "right".
herbelin
2009-08-02
*
Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"
letouzey
2009-07-24
*
Simplify eauto and fix it for compatibility, allowing full delta during
msozeau
2009-07-14
*
Use the proper unification flags in e_exact. This makes exact fail a bit
msozeau
2009-07-09
*
Simplify addition of hints to a hint_db. Rebuild the dnet associated
msozeau
2009-07-08
*
Reactivation of pattern unification of evars in apply unification, in
herbelin
2009-07-08
*
Jolification : tentative de supprimer les "( evd)" et associƩs qui
aspiwack
2009-07-07
*
Add new variants of [rewrite] and [autorewrite] which differ in the
msozeau
2009-06-30
*
Raise an error and not an anomaly if a rewrite is attempted on a
msozeau
2009-06-28
*
Correct treatment of dependent products in signatures: create the evars
msozeau
2009-06-22
*
Fix "unsatisfiable constraints" error messages to include all the
msozeau
2009-06-18
*
Reimplementation of leibniz rewrite to control the instantiation of the
msozeau
2009-06-16
*
Use a lazy value for the message in FailError, so that it won't be
msozeau
2009-06-11
*
When typing a non-dependent arrow, do not put the (anonymous) variable
msozeau
2009-06-11
*
Use the projections for reflexivity, symmetry and transitivity proofs to
msozeau
2009-06-10
*
Correct handling of the initial existentials from the goal and the ones
msozeau
2009-06-09
*
Do a fixpoint on the result of typeclass search to force the
msozeau
2009-06-08
[next]