index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
ltac
/
extratactics.ml4
Commit message (
Expand
)
Author
Age
*
Retyping API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Reductionops API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Termops API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-24
|
\
|
*
Revert 214b9ab7969fae71dcf553c399cb1674e463d0e3
Matthieu Sozeau
2016-10-21
|
*
Fix bug #5036 autorewrite, sections and universes
Matthieu Sozeau
2016-10-20
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-02
|
\
\
|
*
|
Fix bug #5036 autorewrite, sections and universes
Matthieu Sozeau
2016-09-29
|
|
/
*
|
Merging Stdarg and Constrarg.
Pierre-Marie Pédrot
2016-09-21
*
|
Moving Ltac-specific generic arguments to their own file in the ltac/ folder.
Pierre-Marie Pédrot
2016-09-15
*
|
Moving Ltac-specific parsing API to ltac/ folder.
Pierre-Marie Pédrot
2016-09-14
*
|
Unplugging Pptactic from Ppvernac.
Pierre-Marie Pédrot
2016-09-08
|
/
*
Fix bug #4893: not_evar: unexpected failure in 8.5pl1.
Pierre-Marie Pédrot
2016-08-30
*
Merge branch 'v8.5' into trunk
Maxime Dénès
2016-07-04
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
Giving a more natural semantics to injection by default.
Hugo Herbelin
2016-06-18
*
Exporting a generic argument induction_arg. As a consequence,
Hugo Herbelin
2016-06-18
*
Adding eintros to respect the e- prefix policy.
Hugo Herbelin
2016-06-18
*
Purely refactoring and code/API cleanup.
Matthieu Sozeau
2016-06-16
*
Merge PR #195: Complete is_* family of term-examining tactics.
Pierre-Marie Pédrot
2016-06-16
|
\
|
*
Add is_const
Jason Gross
2016-06-16
|
*
Add is_ind, is_constructor, is_proj
Jason Gross
2016-06-07
*
|
STM: proof block detection/error resilience API
Enrico Tassi
2016-06-06
|
/
*
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
*
Put the "specialize_eq" tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
*
Put the "generalize" tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
*
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-05-08
*
Removing useless generic arguments.
Pierre-Marie Pédrot
2016-05-04
*
More toplevel value representation sharing.
Pierre-Marie Pédrot
2016-05-04
*
Moving the Val module to Geninterp.
Pierre-Marie Pédrot
2016-05-04
*
Removing redundant *_TYPED AS clauses in EXTEND statements.
Pierre-Marie Pédrot
2016-04-12
*
Making Autorewrite independent from Ltac.
Pierre-Marie Pédrot
2016-03-25
*
Moving type_uconstr to Pretyping.
Pierre-Marie Pédrot
2016-03-25
*
Creating a dedicated ltac/ folder for Hightactics.
Pierre-Marie Pédrot
2016-03-21
Pierre-Marie Pédrot
Matthieu Sozeau
Maxime Dénès
Pierre Letouzey
Hugo Herbelin
Jason Gross
Enrico Tassi
Emilio Jesus Gallego Arias