index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
plugins
/
micromega
Age
Commit message (
Expand
)
Author
2018-11-23
s/let _ =/let () =/ in some places (mostly goptions related)
Gaëtan Gilbert
2018-10-17
[micromega] Build csdpcert
Emilio Jesus Gallego Arias
2018-10-16
[micromega] remove dead code
Vincent Laporte
2018-10-10
[coqlib] Rebindable Coqlib namespace.
Emilio Jesus Gallego Arias
2018-10-09
Refactoring of Micromega code using a Simplex linear solver
Frédéric Besson
2018-09-24
[engine] Remove and deprecate `nf_enter` et al.
Emilio Jesus Gallego Arias
2018-09-05
[build] Preliminary support for building Coq with `dune`.
Emilio Jesus Gallego Arias
2018-07-18
Merge PR #7897: Remove fourier plugin
Enrico Tassi
2018-07-17
Remove fourier plugin
Maxime Dénès
2018-07-14
[build] Build Coq and plugins with `-strict-sequence`
Emilio Jesus Gallego Arias
2018-07-02
Moving various ml4 files to mlg.
Pierre-Marie Pédrot
2018-06-12
[api] Misctypes removal: several moves:
Emilio Jesus Gallego Arias
2018-06-07
Micromega clean-up
Maxime Dénès
2018-05-30
[api] Remove deprecated object from `Term`
Emilio Jesus Gallego Arias
2018-05-17
Split off Universes functions dealing with generating new universes.
Gaëtan Gilbert
2018-03-23
Deprecate undocumented "intros until 0" in favor of "intros *".
Hugo Herbelin
2018-03-09
[located] More work towards using CAst.t
Emilio Jesus Gallego Arias
2018-03-07
[stdlib] Do not use “Require” inside sections
Vincent Laporte
2018-02-27
Update headers following #6543.
Théo Zimmermann
2018-02-17
Change references to CAMLP4 to CAMLP5 to be more accurate since we no
Jim Fehrle
2017-12-20
Merge PR #6234: Make the micromega extraction check a regular output test.
Maxime Dénès
2017-12-05
Replacing Hashtbl.add by Hashtbl.replace in micromega cache building.
Hugo Herbelin
2017-11-28
Make the micromega extraction check a regular output test.
Gaëtan Gilbert
2017-11-21
[printing] Deprecate all printing functions accessing the global proof.
Emilio Jesus Gallego Arias
2017-11-16
Fix micromega.ml to match generated file and enforce match in make.
Gaëtan Gilbert
2017-11-06
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-10-05
[ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.
Emilio Jesus Gallego Arias
2017-09-28
Efficient fresh name generation relying on sets.
Pierre-Marie Pédrot
2017-07-17
[API] Remove `open API` in ml files in favor of `-open API` flag.
Emilio Jesus Gallego Arias
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-14
Prelude : no more autoload of plugins extraction and recdef
Pierre Letouzey
2017-06-14
Makefile.build : cleanup now that micromega.ml isn't generated + sync check o...
Pierre Letouzey
2017-06-12
Store plugins/micromega/micromega.{ml,mli} files in the repository. Try to ge...
Matej Košík
2017-06-12
Merge PR#709: Bytecode compilation apart from 'make world', again
Maxime Dénès
2017-06-12
Merge PR#718: API cleanup: aliases
Maxime Dénès
2017-06-10
Remove remaining vo.itarget files (obsolete since PR #499)
Pierre Letouzey
2017-06-10
Remove (useless) aliases from the API.
Matej Košík
2017-06-07
Put all plugins behind an "API".
Matej Kosik
2017-06-06
Remove the Sigma (monotonous state) API.
Maxime Dénès
2017-06-01
Break circular dependency in MExtraction
Jason Gross
2017-06-01
extract "plugins/micromega/micromega.ml{,i}" files from "plugins/micromega/ME...
Matej Kosik
2017-05-30
Makefile: no bytecode compilation in make world, see make byte instead
Pierre Letouzey
2017-05-27
[coqlib] Move `Coqlib` to `library/`.
Emilio Jesus Gallego Arias
2017-05-25
Merge PR#481: [option] Remove support for non-synchronous options.
Maxime Dénès
2017-05-24
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-04-27
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
[prev]
[next]