index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
vernacentries.ml
Commit message (
Expand
)
Author
Age
...
*
- Add "Show Universes" to print information about universes during a proof.
Matthieu Sozeau
2014-06-16
*
Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...
Matthieu Sozeau
2014-06-10
*
Adding a toplevel option allowing to deactivate the term sharing in kernel
Pierre-Marie Pédrot
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-06-08
*
Adding a new Control file centralizing the control options of Coq.
Pierre-Marie Pédrot
2014-06-07
*
Remove the syntax [Vernac1. Vernac2. … Vernacn. ].
Arnaud Spiwack
2014-06-06
*
- Fix bug preventing apply from unfolding Fixpoints.
Matthieu Sozeau
2014-05-06
*
Adapt Y. Bertot's path on private inductives (now the keyword is "Private").
Yves Bertot
2014-05-06
*
- Fix handling of polymorphic inductive elimination schemes.
Matthieu Sozeau
2014-05-06
*
- Fix Check to use the constraints inferred during type inference.
Matthieu Sozeau
2014-05-06
*
Initial work on reintroducing old-style polymorphism for compatibility (the s...
Matthieu Sozeau
2014-05-06
*
Correct rebase on STM code. Thanks to E. Tassi for help on dealing with
Matthieu Sozeau
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Adding a stm/ folder, as asked during last workgroup. It was essentially moving
Pierre-Marie Pédrot
2014-04-25
*
Fixing various backtrace recordings.
Pierre-Marie Pédrot
2014-04-25
*
Add an option -Q (tentative name).
Guillaume Melquiond
2014-04-08
*
Adding a Print Strategy vernacular command. It allows to check the
Pierre-Marie Pédrot
2014-03-19
*
Using Hashmaps by default in constant and inductive maps. This changes fold and
Pierre-Marie Pédrot
2014-03-07
*
Using HMaps in Safe_env.environments, hopefully improving performances.
Pierre-Marie Pédrot
2014-03-05
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
CoqIDE: print message of "Fail" command
Enrico Tassi
2014-02-26
*
Simpl_behaviour becomes Reductionops.ReductionBehaviour
Pierre Boutillier
2014-02-24
*
Timeout and Set Default Timeout fixed (closes: #3229)
Enrico Tassi
2014-02-10
*
Removing the [Require "file"] syntax.
Pierre-Marie Pédrot
2014-02-02
*
Load implemented in CoqIDE/STM (closes: #3223)
Enrico Tassi
2014-01-30
*
Make Require verbose
Pierre Boutillier
2014-01-13
*
Proof_using: new syntax + suggestion
Enrico Tassi
2014-01-05
*
Notations can now accept dummy arguments. If ever a bound variable is not
Pierre-Marie Pédrot
2013-12-22
*
Removing the need of evarmaps in constr internalization.
Pierre-Marie Pédrot
2013-12-17
*
The commands that initiate proofs are now in charge of what happens when proo...
Arnaud Spiwack
2013-12-04
*
Centralizing the Ltac-defining functions in Tacenv.
ppedrot
2013-11-10
*
Made multiple-goal tactic work after all: .
aspiwack
2013-11-02
*
Fixes parsing of all: followed by a typechecking/evaluation command.
aspiwack
2013-11-02
*
Adds a new goal selector "all:".
aspiwack
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-11-02
*
Conv_orable made functional and part of pre_env
gareuselesinge
2013-10-31
*
cList: a few alternative to hashtbl-based uniquize, distinct, subset
letouzey
2013-10-23
*
cList: set-as-list functions are now with an explicit comparison
letouzey
2013-10-23
*
declaration_hooks use Ephemeron
gareuselesinge
2013-10-18
*
Remove some uses of local modules (some were unused, some were costly).
xclerc
2013-10-14
*
STM: fix verbosity of queries
gareuselesinge
2013-10-07
*
Moving side effects into evar_map. There was no reason to keep another
ppedrot
2013-10-05
*
Removing a bunch of generic equalities.
ppedrot
2013-09-27
*
get rid of closures in global/proof state
gareuselesinge
2013-08-08
*
Support Proof General
gareuselesinge
2013-08-08
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Replacing uses of association lists by maps in notations.
ppedrot
2013-08-03
*
Added a Print Debug GC command that displays the current state of
ppedrot
2013-08-01
[prev]
[next]