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
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-09
|
\
*
|
Redo fix init_setoid -> init_relation_classes
Matthieu Sozeau
2016-03-09
|
*
Fix strategy of Keyed Unification
Matthieu Sozeau
2016-03-09
*
|
Moving Autorewrite to Hightatctic.
Pierre-Marie Pédrot
2016-03-06
*
|
Putting Tactic_debug just below Tacinterp.
Pierre-Marie Pédrot
2016-03-06
*
|
Removing dependency of Himsg in tactic files.
Pierre-Marie Pédrot
2016-03-06
*
|
Moving Tactic_debug to tactics/ folder.
Pierre-Marie Pédrot
2016-03-06
*
|
Moving Ltac traces to Tacexpr and Tacinterp.
Pierre-Marie Pédrot
2016-03-06
*
|
Removing useless grammar.cma dependencies.
Pierre-Marie Pédrot
2016-03-06
*
|
Moving Eauto to a simple ML file.
Pierre-Marie Pédrot
2016-03-06
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-05
|
\
|
*
|
Exporting build_selector, a component of discriminate, for use in congruence.
Hugo Herbelin
2016-03-05
*
|
Adding some standard arguments in tactic scopes.
Pierre-Marie Pédrot
2016-03-04
*
|
Replacing ad-hoc tactic scopes by generic ones using [create_ltac_quotations].
Pierre-Marie Pédrot
2016-03-04
*
|
Removing the UConstr entry of the tactic_arg AST.
Pierre-Marie Pédrot
2016-03-04
*
|
Moving the "move" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
Moving the "exists" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
Moving the "symmetry" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
Moving the "generalize dependent" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
Moving the "clearbody" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
Moving the "clear" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
Moving the "cofix" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
Moving the "fix" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
|
*
Fixing bug #4596: [rewrite] broke in the past few weeks.
Pierre-Marie Pédrot
2016-02-28
*
|
Removing Tacmach.New qualification in Tacinterp.
Pierre-Marie Pédrot
2016-02-27
*
|
Removing some compatibility layers in Tacinterp.
Pierre-Marie Pédrot
2016-02-27
*
|
Removing the MetaIdArg entry of tactic expressions.
Pierre-Marie Pédrot
2016-02-24
*
|
Getting rid of the "<:tactic< ... >>" quotations.
Pierre-Marie Pédrot
2016-02-24
*
|
Moving tauto.ml4 to a proper ML file.
Pierre-Marie Pédrot
2016-02-23
|
*
Fix bug #4544: Backtrack on using full betaiota reduction during keyed unific...
Matthieu Sozeau
2016-02-23
*
|
Moving the Tauto tactic to proper Ltac.
Pierre-Marie Pédrot
2016-02-22
*
|
The tactic generic argument now returns a value rather than a glob_expr.
Pierre-Marie Pédrot
2016-02-22
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-02-21
|
\
|
|
*
Fix regression from 8.4 in reflexivity/...
Matthieu Sozeau
2016-02-19
*
|
FIX: of my previous merging mistake
Matej Kosik
2016-02-18
|
*
Fix bug #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity").
Pierre-Marie Pédrot
2016-02-17
*
|
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-17
|
\
\
*
|
|
Tacticals: typo in a comment
Pierre Letouzey
2016-02-16
|
*
|
merging conflicts with the original "trunk__CLEANUP__Context__2" branch
Matej Kosik
2016-02-15
|
/
|
|
*
|
|
Using monotonic types for conversion functions.
Pierre-Marie Pédrot
2016-02-15
*
|
|
Code factorization of tactic "unfold_body".
Pierre-Marie Pédrot
2016-02-15
*
|
|
More conversion functions in the new tactic API.
Pierre-Marie Pédrot
2016-02-15
*
|
|
Moving conversion functions to the new tactic API.
Pierre-Marie Pédrot
2016-02-15
*
|
|
Renaming functions in Typing to stick to the standard e_* scheme.
Pierre-Marie Pédrot
2016-02-15
*
|
|
Monotonizing the Evarutil module.
Pierre-Marie Pédrot
2016-02-15
|
*
|
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
|
/
/
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-29
|
\
|
|
*
Fix bug #4537: Coq 8.5 is slower in typeclass resolution.
Pierre-Marie Pédrot
2016-01-27
|
*
Fixing bug #4511: evar tactic can create non-typed evars.
Pierre-Marie Pédrot
2016-01-24
|
*
Implement support for universe binder lists in Instance and Program Fixpoint/...
Matthieu Sozeau
2016-01-23
[next]