index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
funind
/
invfun.ml
Commit message (
Expand
)
Author
Age
...
*
Reorganisation of intropattern code
Hugo Herbelin
2014-08-18
*
Reorganization of tactics:
Hugo Herbelin
2014-08-18
*
Experimentally adding an option for automatically erasing an
Hugo Herbelin
2014-08-05
*
Proofs now take and return an evar_universe_context, simplifying interfaces
Matthieu Sozeau
2014-06-18
*
Passing some tactics to the new monad type.
Pierre-Marie Pédrot
2014-06-12
*
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-06-08
*
Fix funind w.r.t. universes
Matthieu Sozeau
2014-05-06
*
- Fix bug preventing apply from unfolding Fixpoints.
Matthieu Sozeau
2014-05-06
*
Adapt universe polymorphic branch to new handling of futures for delayed proofs.
Matthieu Sozeau
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
The commands that initiate proofs are now in charge of what happens when proo...
Arnaud Spiwack
2013-12-04
*
Remove the Hiddentac module.
Arnaud Spiwack
2013-11-25
*
The tactic [admit] exits with the "unsafe" status.
aspiwack
2013-11-02
*
Makes the new Proofview.tactic the basic type of Ltac.
aspiwack
2013-11-02
*
Rtree : cleanup of the comparing code
letouzey
2013-10-24
*
declaration_hooks use Ephemeron
gareuselesinge
2013-10-18
*
Removing a bunch of generic equalities.
ppedrot
2013-09-27
*
recdef: restore old semantics (pre STM)
gareuselesinge
2013-08-30
*
Fix typo in error message
gareuselesinge
2013-08-30
*
get rid of closures in global/proof state
gareuselesinge
2013-08-08
*
State Transaction Machine
gareuselesinge
2013-08-08
*
States: frozen states can hold closures
gareuselesinge
2013-05-06
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Restrict (try...with...) to avoid catching critical exn (part 15)
letouzey
2013-03-13
*
Restrict (try...with...) to avoid catching critical exn (part 11)
letouzey
2013-03-13
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
Modulification of Label
ppedrot
2012-12-18
*
Modulification of identifier
ppedrot
2012-12-14
*
correcting a little bug in Function
jforest
2012-10-31
*
Fixing a bug introduced in Funind plugin when reorganizing the CList
ppedrot
2012-09-24
*
More cleaning on Utils and CList. Some parts of the code being
ppedrot
2012-09-17
*
Some documentation and cleaning of CList and Util interfaces.
ppedrot
2012-09-15
*
As r15801: putting everything from Util.array_* to CArray.*.
ppedrot
2012-09-14
*
Moving Utils.list_* to a proper CList module, which includes stdlib
ppedrot
2012-09-14
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
Getting rid of Pp.msgnl and Pp.message.
ppedrot
2012-06-01
*
Getting rid of Pp.msg
ppedrot
2012-05-30
*
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
*
locus.mli for occurrences+clauses, misctypes.mli for various little things
letouzey
2012-05-29
*
correct abort in Function when a proof of inversion fails
letouzey
2012-04-23
*
A unified backtrack mechanism, with a basic "Show Script" as side-effect
letouzey
2012-03-23
*
Noise for nothing
pboutill
2012-03-02
*
various corrections in invfun due to a modification in induction
jforest
2012-03-01
*
correcting a little bug in invfun.ml
jforest
2012-02-29
*
Fixing Equality.injectable which did not detect an equality without
herbelin
2011-10-22
*
correction du bug 2047
jforest
2011-09-09
[prev]
[next]