index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
btauto
/
refl_btauto.ml
Commit message (
Expand
)
Author
Age
*
[api] Remove deprecated object from `Term`
Emilio Jesus Gallego Arias
2018-05-30
*
Split off Universes functions dealing with generating new universes.
Gaëtan Gilbert
2018-05-17
*
[printing] Deprecate all printing functions accessing the global proof.
Emilio Jesus Gallego Arias
2017-11-21
*
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
*
[API] Remove `open API` in ml files in favor of `-open API` flag.
Emilio Jesus Gallego Arias
2017-07-17
*
Put all plugins behind an "API".
Matej Kosik
2017-06-07
*
Remove the Sigma (monotonous state) API.
Maxime Dénès
2017-06-06
*
[coqlib] Deprecate redundant Coqlib functions.
Emilio Jesus Gallego Arias
2017-05-27
*
Reductionops now return EConstrs.
Pierre-Marie Pédrot
2017-02-14
*
Proofview.Goal primitive now return EConstrs.
Pierre-Marie Pédrot
2017-02-14
*
Eliminating parts of the right-hand side compatibility layer
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
*
Termops API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Moving unused code out of the kernel into Termops.
Pierre-Marie Pédrot
2016-10-31
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
Removing OCaml deprecated function names from the Lazy module.
Pierre-Marie Pédrot
2016-03-10
*
Moving conversion functions to the new tactic API.
Pierre-Marie Pédrot
2016-02-15
*
Boxing the Goal.enter primitive into a record type.
Pierre-Marie Pédrot
2015-10-20
*
Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.
Hugo Herbelin
2014-12-07
*
Change reduction_of_red_expr to return an e_reduction_function returning
Matthieu Sozeau
2014-10-24
*
Renaming goal-entering functions.
Pierre-Marie Pédrot
2014-09-06
*
Reorganization of tactics:
Hugo Herbelin
2014-08-18
*
Fix semantics of change p with c to typecheck c at each specific occurrence o...
Matthieu Sozeau
2014-06-23
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
More Proofview.Goal.enter.
aspiwack
2013-11-02
*
Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.
aspiwack
2013-11-02
*
Getting rid of Goal.here, and all the related exceptions and combinators.
aspiwack
2013-11-02
*
Makes the new Proofview.tactic the basic type of Ltac.
aspiwack
2013-11-02
*
Get rid of polymorphic comparison in "plugins/btauto/refl_btauto.ml".
xclerc
2013-10-24
*
Restrict (try...with...) to avoid catching critical exn (part 9)
letouzey
2013-03-13
*
Replace nat indices with positive one in Btauto.
ppedrot
2012-06-28
*
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-05-29
*
Glob_term now mli-only, operations now in Glob_ops
letouzey
2012-05-29
*
Added an pattern / occurence syntax for vm_compute.
ppedrot
2012-01-30
*
Added a Btauto plugin, that solves boolean tautologies.
ppedrot
2012-01-13