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
*
Removing the last use of valueIn in Tauto.
Pierre-Marie Pédrot
2015-12-04
*
Removing dynamic inclusion of constrs in tactic AST.
Pierre-Marie Pédrot
2015-12-04
*
Removing the globTacticIn primitive.
Pierre-Marie Pédrot
2015-12-03
*
Fixing Tauto compilation for older versions of OCaml.
Pierre-Marie Pédrot
2015-12-03
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-03
|
\
*
|
Removing the last use of tacticIn in setoid_ring.
Pierre-Marie Pédrot
2015-12-03
*
|
Removing the use of tacticIn in Tauto.
Pierre-Marie Pédrot
2015-12-03
|
*
Slight simplification of code for pat/constr.
Hugo Herbelin
2015-12-02
|
*
Dead code from August 2014 in apply in.
Hugo Herbelin
2015-12-02
*
|
Removing dead code in Obligations.
Pierre-Marie Pédrot
2015-12-02
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-29
|
\
|
|
*
Fix [Polymorphic Hint Rewrite].
Matthieu Sozeau
2015-11-27
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-26
|
\
|
|
*
Fix generation of equality schemes on polymorphic equality types.
Matthieu Sozeau
2015-11-23
*
|
Removing a use of old refine in Tactics.
Pierre-Marie Pédrot
2015-11-23
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-20
|
\
|
|
*
Fix bug #4429: eauto with arith: 70x performance regression in Coq 8.5.
Pierre-Marie Pédrot
2015-11-19
|
*
Fix bug #4433, removing hack on evars appearing in a pattern from a
Matthieu Sozeau
2015-11-19
|
*
Improve error message.
Maxime Dénès
2015-11-18
*
|
Inlining the only use of Clenv.connect_clenv.
Pierre-Marie Pédrot
2015-11-18
|
*
More optimizations of [Clenv.clenv_fchain].
Pierre-Marie Pédrot
2015-11-17
|
*
Performance fix for destruct.
Pierre-Marie Pédrot
2015-11-17
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-15
|
\
|
|
*
Continue fix of PMP, handling setoid_rewrite in let-bound hyps correctly.
Matthieu Sozeau
2015-11-13
|
*
Fix bug #3257, setoid_reflexivity should fail if not completing the goal.
Matthieu Sozeau
2015-11-11
*
|
Activating bracketing of last or-and introduction pattern by default
Hugo Herbelin
2015-11-10
*
|
Merge origin/v8.5 into trunk
Hugo Herbelin
2015-11-10
|
\
|
|
*
Typo.
Hugo Herbelin
2015-11-10
|
*
Fix bug #4404: [remember] gives Error: Conversion test raised an anomaly.
Pierre-Marie Pédrot
2015-11-10
*
|
Implementing assert and cut with LetIn rather than using a beta-redex.
Hugo Herbelin
2015-11-07
|
*
Preservation of the name of evars/goals when applying pose/set/intro/clearbody.
Hugo Herbelin
2015-11-07
*
|
Merge remote-tracking branch 'origin/v8.5' into upstream-trunk
Hugo Herbelin
2015-11-07
|
\
|
|
*
Fix bug #4273
Matthieu Sozeau
2015-11-05
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-05
|
\
|
|
*
Hint Cut documentation and cleanup of printing (was duplicated and
Matthieu Sozeau
2015-11-04
|
*
Fix bug in proofs/logic.ml type_of_global_reference_knowing_conclusion
Matthieu Sozeau
2015-11-04
|
*
Fix bug #4397: refreshing types in abstract_generalize.
Matthieu Sozeau
2015-11-02
|
*
Fix bug #4151: discrepancy between exact and eexact/eassumption.
Matthieu Sozeau
2015-11-02
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-30
|
\
|
*
|
Monotonizing Tactics.change_arg.
Pierre-Marie Pédrot
2015-10-29
*
|
Removing some goal unsafeness in Equality.
Pierre-Marie Pédrot
2015-10-29
*
|
Removing unused and useless exported function in Hints.
Pierre-Marie Pédrot
2015-10-29
*
|
Removing the evar_map argument from s_enter.
Pierre-Marie Pédrot
2015-10-29
*
|
Removing some goal unsafeness in inductive schemes.
Pierre-Marie Pédrot
2015-10-29
|
*
Avoid an anomaly when destructing an unknown ident. (Fix bug #4395)
Guillaume Melquiond
2015-10-29
|
*
Fixing another instance of bug #3267 in eauto, this time in the
Hugo Herbelin
2015-10-29
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-29
|
\
|
|
*
Univs: local names handling.
Matthieu Sozeau
2015-10-28
|
*
Avoid type checking private_constants (side_eff) again during Qed (#4357).
Enrico Tassi
2015-10-28
|
*
Preserving goal name in revert/bring_hyps.
Hugo Herbelin
2015-10-26
[next]