index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
plugins
/
funind
/
functional_principles_proofs.ml
Age
Commit message (
Expand
)
Author
2016-03-06
Moving Eauto to a simple ML file.
Pierre-Marie Pédrot
2016-02-15
merging conflicts with the original "trunk__CLEANUP__Context__2" branch
Matej Kosik
2016-02-15
More conversion functions in the new tactic API.
Pierre-Marie Pédrot
2016-02-15
Moving conversion functions to the new tactic API.
Pierre-Marie Pédrot
2016-02-09
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-01-11
merge
Matej Kosik
2016-01-11
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2015-12-28
Eradicating uses of open_constr in TACTIC EXTEND in favour of uconstr.
Pierre-Marie Pédrot
2015-12-05
Removing redundant versions of generalize.
Hugo Herbelin
2015-12-05
Moving three related small half-general half-ad-hoc utility functions
Hugo Herbelin
2015-10-19
Function debug mode more formatted.
Pierre Courtieu
2015-05-13
Safer typing primitives.
Pierre-Marie Pédrot
2015-04-14
Function now supports puniveres
jforest
2015-04-13
correction of a bug reported by Tristan Crolard
jforest
2015-02-14
Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior
Enrico Tassi
2015-02-02
Removing dead code.
Pierre-Marie Pédrot
2014-12-16
Getting rid of Exninfo hacks.
Pierre-Marie Pédrot
2014-11-21
Writing Tactics.keep in the new monad.
Pierre-Marie Pédrot
2014-11-07
Removing the legacy intro tactic code.
Pierre-Marie Pédrot
2014-11-03
Writing rename_hyps in the new monad.
Pierre-Marie Pédrot
2014-10-22
Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.
Arnaud Spiwack
2014-10-13
library/opaqueTables: enable their use in interactive mode
Enrico Tassi
2014-10-07
Splitting out of auto.ml a file hints.ml dedicated to hints so as to
Hugo Herbelin
2014-09-12
Referring to evars by names. Added a parser for evars (but parsing of
Hugo Herbelin
2014-08-18
A reorganization of the "assert" tactics (hopefully uniform naming
Hugo Herbelin
2014-08-18
Reorganization of tactics:
Hugo Herbelin
2014-08-05
Experimentally adding an option for automatically erasing an
Hugo Herbelin
2014-06-18
Proofs now take and return an evar_universe_context, simplifying interfaces
Matthieu Sozeau
2014-06-08
Moving hook code from Future to Lemmas. This seemed to disrupt compilation of
Pierre-Marie Pédrot
2014-06-08
Enforce a correct exception handling in declaration_hooks
Enrico Tassi
2014-05-06
Initial work on reintroducing old-style polymorphism for compatibility (the s...
Matthieu Sozeau
2014-05-06
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-03-01
Fixing pervasive comparisons
Pierre-Marie Pédrot
2014-01-20
bug correction in proving principles of function
jforest
2013-12-04
The commands that initiate proofs are now in charge of what happens when proo...
Arnaud Spiwack
2013-11-25
Remove the Hiddentac module.
Arnaud Spiwack
2013-11-08
Porting Tactics.assumption to the new engine.
ppedrot
2013-11-02
The tactic [admit] exits with the "unsafe" status.
aspiwack
2013-11-02
Makes the new Proofview.tactic the basic type of Ltac.
aspiwack
2013-10-24
More monomorphic List.mem + List.assoc + ...
letouzey
2013-10-23
cList: set-as-list functions are now with an explicit comparison
letouzey
2013-10-18
declaration_hooks use Ephemeron
gareuselesinge
2013-09-27
Removing a bunch of generic equalities.
ppedrot
2013-09-19
Get rid of the uses of deprecated OCaml elements (still remaining compatible ...
xclerc
2013-08-08
get rid of closures in global/proof state
gareuselesinge
2013-04-29
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-02
Revised infrastructure for lazy loading of opaque proofs
letouzey
2013-03-13
Restrict (try...with...) to avoid catching critical exn (part 11)
letouzey
2013-03-13
Restrict (try...with...) to avoid catching critical exn (part 9)
letouzey
2013-03-13
Restrict (try...with...) to avoid catching critical exn (part 7)
letouzey
[next]
