aboutsummaryrefslogtreecommitdiff
path: root/plugins/fourier
AgeCommit message (Expand)Author
2018-09-05[build] Preliminary support for building Coq with `dune`.Emilio Jesus Gallego Arias
2018-07-17Remove fourier pluginMaxime Dénès
2018-07-02Moving various ml4 files to mlg.Pierre-Marie Pédrot
2018-05-17Split off Universes functions dealing with generating new universes.Gaëtan Gilbert
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-17Change references to CAMLP4 to CAMLP5 to be more accurate since we noJim Fehrle
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-07-17[API] Remove `open API` in ml files in favor of `-open API` flag.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-12Merge PR#718: API cleanup: aliasesMaxime Dénès
2017-06-10Remove remaining vo.itarget files (obsolete since PR #499)Pierre Letouzey
2017-06-10Remove (useless) aliases from the API.Matej Košík
2017-06-07Put all plugins behind an "API".Matej Kosik
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-05-29Merge PR#512: [cleanup] Unify all calls to the error function.Maxime Dénès
2017-05-27[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[coqlib] Deprecate redundant Coqlib functions.Emilio Jesus Gallego Arias
2017-04-24Fix the API of the new pf_constr_of_global.Pierre-Marie Pédrot
2017-03-24Merge branch 'trunk' into pr379Maxime Dénès
2017-03-22Change the parser and printer so that they use IZR for real constants.Guillaume Melquiond
2017-02-17Moving the Ltac plugin to a pack-based one.Pierre-Marie Pédrot
2017-02-14Definining EConstr-based contexts.Pierre-Marie Pédrot
2017-02-14Removing compatibility layers from TacticalsPierre-Marie Pédrot
2017-02-14Proofview.Goal primitive now return EConstrs.Pierre-Marie Pédrot
2017-02-14Eliminating parts of the right-hand side compatibility layerPierre-Marie Pédrot
2017-02-14Equality API using EConstr.Pierre-Marie Pédrot
2017-02-14Tactics API using EConstr.Pierre-Marie Pédrot
2017-02-14Termops API using EConstr.Pierre-Marie Pédrot
2016-10-31Moving unused code out of the kernel into Termops.Pierre-Marie Pédrot
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-08Compilation via pack for plugins of the stdlibPierre Letouzey
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-12-30Simplifying code of fourier.Hugo Herbelin
2015-10-20Boxing the Goal.enter primitive into a record type.Pierre-Marie Pédrot
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-12-09Switch the few remaining iso-latin-1 files to utf8Pierre Letouzey
2014-12-07Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.Hugo Herbelin
2014-09-06Renaming goal-entering functions.Pierre-Marie Pédrot
2014-08-18Reorganization of tactics:Hugo Herbelin
2014-06-23Fix semantics of change p with c to typecheck c at each specific occurrence o...Matthieu Sozeau
2014-06-12Passing some tactics to the new monad type.Pierre-Marie Pédrot
2014-05-12Now parsing rules of ML-declared tactics are only made available after thePierre-Marie Pédrot
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:38:52 +0000