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
*
Fix some typos.
Guillaume Melquiond
2015-10-13
*
Remove code that was already commented out.
Maxime Dénès
2015-10-12
*
Fixing bug #4366: Conversion tactics recheck uselessly convertibility.
Pierre-Marie Pédrot
2015-10-11
*
Fixing untimely unexpected warning "Collision between bound variables" (#4317).
Hugo Herbelin
2015-10-11
*
Refine fix for handling of the universe contexts of hints, depending on
Matthieu Sozeau
2015-10-09
*
Fix CFGV contrib: handling of global hints introducing global universes.
Matthieu Sozeau
2015-10-09
*
Fix bug #4354: interpret hints in the right env and sigma.
Matthieu Sozeau
2015-10-06
*
Univs: refined handling of assumptions
Matthieu Sozeau
2015-10-02
*
Univs: fix evar_map handling in Hint processing.
Matthieu Sozeau
2015-10-02
*
discriminate: Do fresh_global in the right env in presence of side-effects.
Matthieu Sozeau
2015-10-02
*
Univs: fix many evar_map initializations and leaks.
Matthieu Sozeau
2015-10-02
*
Hopefully better names to constructors of internal_flag, as discussed
Hugo Herbelin
2015-09-23
*
Give a way to control if the decidable-equality schemes are built like
Hugo Herbelin
2015-09-23
*
Fixing bug #4207: setoid_rewrite creates self-referring hypotheses.
Pierre-Marie Pédrot
2015-09-22
*
In pat/constr introduction patterns, fixing in a better way clearing problems
Hugo Herbelin
2015-09-16
*
Continuing investigation on how to preserve the locality of the action
Hugo Herbelin
2015-09-16
*
Univs: Add universe binding lists to definitions
Matthieu Sozeau
2015-09-14
*
Fixing incomplete bugfix in 76f27140e6e34 (unfortunately 5 commits
Hugo Herbelin
2015-09-08
*
Ensuring that patterns of the form pat/constr move the hypotheses replacing
Hugo Herbelin
2015-09-08
*
Short cosmetic changes in tactics.ml.
Hugo Herbelin
2015-09-08
*
A bit of documentation of OCaml code for intro_patterns.
Hugo Herbelin
2015-09-08
*
New option "Unset Bracketing Last Introduction Pattern" for preserving
Hugo Herbelin
2015-09-08
*
Fixing clearing of temporary hypotheses with intro pattern pat/constr.
Hugo Herbelin
2015-09-08
*
Fixing "pose proof (H ...) as H" and "assert (H:=H ...) which were supposed
Hugo Herbelin
2015-09-08
*
Reverting 16 last commits, committed mistakenly using the wrong push command.
Hugo Herbelin
2015-08-02
*
Give a way to control if the decidable-equality schemes are built like
Hugo Herbelin
2015-08-02
*
Granting Jason's request for an ad hoc compatibility option on
Hugo Herbelin
2015-08-02
*
Fix for bug #4280: "decide equality produces terms that don't compute well".
Pierre-Marie Pédrot
2015-07-28
*
Fixing bug #3509 and #3510 (anomalies in "tactics/term_dnet.ml").
Pierre-Marie Pédrot
2015-07-28
*
class_tactics: make interruptible
Enrico Tassi
2015-06-29
*
class_tactics: remove catch-all, use Errors.noncritical
Enrico Tassi
2015-06-29
*
Fixing incompatibility introduced with simpl in commit 364decf59c1 (or
Hugo Herbelin
2015-06-23
*
With the field record punning syntax.
Theo Zimmermann
2015-06-23
*
Put all arguments of strategy in record.
Theo Zimmermann
2015-06-23
*
Strategy is now a record type with a function field.
Theo Zimmermann
2015-06-23
*
Add comments.
Theo Zimmermann
2015-06-23
*
Fix bug #4159
Matthieu Sozeau
2015-05-27
*
Fixing bug #2814: "Anomaly: Uncaught exception Option.IsNone".
Pierre-Marie Pédrot
2015-05-16
*
Granting wish #4048: Locate Ltac prints the source of redefined Ltac.
Pierre-Marie Pédrot
2015-05-15
*
Fixing bug #4216:
Pierre-Marie Pédrot
2015-05-13
*
Safer typing primitives.
Pierre-Marie Pédrot
2015-05-13
*
Adding an option Loose Hint Behavior to handle hints loaded but not imported.
Pierre-Marie Pédrot
2015-05-12
*
Adding unique identifiers to hints.
Pierre-Marie Pédrot
2015-05-12
*
Adding a test to check whether two tactic notations conflict.
Pierre-Marie Pédrot
2015-05-11
*
Fixing bug #4232.
Pierre-Marie Pédrot
2015-05-11
*
Rationalizing a bit the interface of Hints.
Pierre-Marie Pédrot
2015-05-11
*
Adding a flag "Set Regular Subst Tactic" off by default in v8.5 for
Hugo Herbelin
2015-05-09
*
Fixing treatment of recursive equations damaged by 857e82b2ca0d1.
Hugo Herbelin
2015-05-06
*
Fixing "subst" to respect v8.4 most-ancient to most-recent hyps order
Hugo Herbelin
2015-05-06
*
Removing dead code in Rewrite.
Pierre-Marie Pédrot
2015-05-05
[next]