index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
omega
Commit message (
Expand
)
Author
Age
*
Put all plugins behind an "API".
Matej Kosik
2017-06-07
*
Remove the Sigma (monotonous state) API.
Maxime Dénès
2017-06-06
*
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-02
*
Cleanup: removal of constr_of_global.
Matthieu Sozeau
2017-05-29
*
Merge PR#512: [cleanup] Unify all calls to the error function.
Maxime Dénès
2017-05-29
|
\
|
*
[cleanup] Unify all calls to the error function.
Emilio Jesus Gallego Arias
2017-05-27
*
|
[coqlib] Move `Coqlib` to `library/`.
Emilio Jesus Gallego Arias
2017-05-27
|
/
*
Merge PR#666: romega revisited : no more normalization trace, cleaned-up reso...
Maxime Dénès
2017-05-26
|
\
*
|
[option] Remove support for non-synchronous options.
Emilio Jesus Gallego Arias
2017-05-24
|
*
refl_omega: some code refactoring
Pierre Letouzey
2017-05-22
|
*
ROmega : merge O_CONSTANT* into a single O_BAD_CONSTANT
Pierre Letouzey
2017-05-22
|
/
*
Fix 4.04 warnings
Gaetan Gilbert
2017-04-27
*
Porting omega to the new tactic API.
Pierre-Marie Pédrot
2017-04-24
*
Removing trivial compatibility layer in omega.
Pierre-Marie Pédrot
2017-04-24
*
Fix an unhandled exception in Omega.
Pierre-Marie Pédrot
2017-04-07
*
Actually exporting delayed universes in the EConstr implementation.
Pierre-Marie Pédrot
2017-04-01
*
Merge branch 'trunk' into pr379
Maxime Dénès
2017-03-24
|
\
|
*
Moving the Ltac plugin to a pack-based one.
Pierre-Marie Pédrot
2017-02-17
*
|
Removing most nf_enter in tactics.
Pierre-Marie Pédrot
2017-02-14
*
|
Fix a mishandled exception in Omega.
Pierre-Marie Pédrot
2017-02-14
*
|
Definining EConstr-based contexts.
Pierre-Marie Pédrot
2017-02-14
*
|
Omega API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Removing various compatibility layers of tactics.
Pierre-Marie Pédrot
2017-02-14
*
|
Reductionops now return EConstrs.
Pierre-Marie Pédrot
2017-02-14
*
|
Proofview.Goal primitive now return EConstrs.
Pierre-Marie Pédrot
2017-02-14
*
|
Contradiction API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Tactics API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Tacmach API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Reductionops API using EConstr.
Pierre-Marie Pédrot
2017-02-14
|
/
*
Merging Stdarg and Constrarg.
Pierre-Marie Pédrot
2016-09-21
*
CLEANUP: minor readability improvements
Matej Kosik
2016-08-24
*
CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" function
Matej Kosik
2016-08-24
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
Compilation via pack for plugins of the stdlib
Pierre Letouzey
2016-06-08
*
Removing the old refine tactic from the Tactics module.
Pierre-Marie Pédrot
2016-05-17
*
Put the "generalize" tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
*
Put the "clear" tactic into the monad.
Pierre-Marie Pédrot
2016-05-16
*
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-05-08
*
Removing the special status of generic entries defined by Coq itself.
Pierre-Marie Pédrot
2016-03-17
*
Getting rid of the "<:tactic< ... >>" quotations.
Pierre-Marie Pédrot
2016-02-24
*
merging conflicts with the original "trunk__CLEANUP__Context__2" branch
Matej Kosik
2016-02-15
|
\
*
|
Moving conversion functions to the new tactic API.
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-21
|
\
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
Boxing the Goal.enter primitive into a record type.
Pierre-Marie Pédrot
2015-10-20
|
/
*
Fix some typos.
Guillaume Melquiond
2015-10-13
*
Safer typing primitives.
Pierre-Marie Pédrot
2015-05-13
*
Using tclZEROMSG instead of tclZERO in several places.
Pierre-Marie Pédrot
2015-04-23
*
Accomodating #4166 (providing "Require Import OmegaTactic" as a
Hugo Herbelin
2015-04-01
[next]