index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
micromega
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
*
Break circular dependency in MExtraction
Jason Gross
2017-06-01
*
extract "plugins/micromega/micromega.ml{,i}" files from "plugins/micromega/ME...
Matej Kosik
2017-06-01
*
[coqlib] Move `Coqlib` to `library/`.
Emilio Jesus Gallego Arias
2017-05-27
*
Merge PR#481: [option] Remove support for non-synchronous options.
Maxime Dénès
2017-05-25
|
\
*
\
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-24
|
\
\
|
|
*
[option] Remove support for non-synchronous options.
Emilio Jesus Gallego Arias
2017-05-24
|
|
/
|
*
Remove unused [open] statements
Gaetan Gilbert
2017-04-27
|
*
Micromega: do not use Filename.temp_dir_path, remove unused values
Gaetan Gilbert
2017-04-27
|
*
Rename Sos_lib.(||) -> parser_or to avoid (deprecated) Pervasives.or
Gaetan Gilbert
2017-04-27
|
*
Disambiguate Polynomial.Hyp and Mfourier.Hyp -> Assum
Gaetan Gilbert
2017-04-27
*
|
[location] Remove Loc.ghost.
Emilio Jesus Gallego Arias
2017-04-25
|
*
Removing tactic compatibility layer in Micromega.
Pierre-Marie Pédrot
2017-04-24
|
/
*
Merge branch 'trunk' into pr379
Maxime Dénès
2017-03-24
|
\
|
*
Remove duplicate lemmas.
Guillaume Melquiond
2017-03-22
|
*
Micromega: removing a constant preventing micromega to be loaded before Logic.v.
Hugo Herbelin
2017-03-09
|
*
Moving the Ltac plugin to a pack-based one.
Pierre-Marie Pédrot
2017-02-17
*
|
Merge branch 'master'.
Pierre-Marie Pédrot
2017-02-14
|
\
|
*
|
Micromega API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Removing various compatibility layers of tactics.
Pierre-Marie Pédrot
2017-02-14
*
|
Removing compatibility layers in Retyping
Pierre-Marie Pédrot
2017-02-14
*
|
Tactics API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
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-11-30
|
/
|
|
*
Lazily load constants in micromega (bug #5134).
Guillaume Melquiond
2016-11-24
*
|
Merging Stdarg and Constrarg.
Pierre-Marie Pédrot
2016-09-21
*
|
Make the Coq codebase independent from Ltac-related code.
Pierre-Marie Pédrot
2016-09-16
|
\
\
|
|
/
|
/
|
|
*
Moving Ltac-specific generic arguments to their own file in the ltac/ folder.
Pierre-Marie Pédrot
2016-09-15
*
|
Fix Bug #5073 : regression of micromega plugin
Frédéric Besson
2016-09-08
*
|
Fix Bug #5073 : regression of micromega plugin
Frédéric Besson
2016-09-08
|
/
*
micromega : more robust generation of proof terms
Frédéric Besson
2016-09-07
*
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-09-02
|
\
*
|
Fixed Bug #5003 : more careful generalisation of dependent terms.
Frédéric Besson
2016-09-01
*
|
Fix Bug #5005 : micromega tactics is now robust to failure of 'abstract'.
Frédéric Besson
2016-08-31
*
|
plugin micromega : nra also handles non-linear rational arithmetic over Q (Fi...
Frédéric Besson
2016-08-30
|
*
micromega cache files are now hidden files (cf #4156)
Frédéric Besson
2016-08-30
*
|
Fix bug #4923: Warning: appcontext is deprecated.
Pierre-Marie Pédrot
2016-07-18
*
|
Revert "Merge remote-tracking branch 'github/pr/229' into trunk"
Maxime Dénès
2016-07-05
*
|
Merge remote-tracking branch 'github/pr/229' 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
|
*
|
Makefile: no bytecode compilation in make world, see make byte instead
Pierre Letouzey
2016-06-29
|
/
/
*
|
Giving a more natural semantics to injection by default.
Hugo Herbelin
2016-06-18
*
|
Compilation via pack for plugins of the stdlib
Pierre Letouzey
2016-06-08
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-06-01
|
\
|
*
|
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
|
*
Disable memoization rather than failing when files cannot be opened.
Guillaume Melquiond
2016-05-20
*
|
Micromega: qualify Coq.micromega.Tauto (avoid coqdep warnings about new Init/...
Pierre Letouzey
2016-05-19
[next]