aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernacentries.ml
Commit message (Expand)AuthorAge
...
* - Add "Show Universes" to print information about universes during a proof.Gravatar Matthieu Sozeau2014-06-16
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Gravatar Matthieu Sozeau2014-06-10
* Adding a toplevel option allowing to deactivate the term sharing in kernelGravatar Pierre-Marie Pédrot2014-06-08
* Moving hook code from Future to Lemmas. This seemed to disrupt compilation ofGravatar Pierre-Marie Pédrot2014-06-08
* Enforce a correct exception handling in declaration_hooksGravatar Enrico Tassi2014-06-08
* Adding a new Control file centralizing the control options of Coq.Gravatar Pierre-Marie Pédrot2014-06-07
* Remove the syntax [Vernac1. Vernac2. … Vernacn. ].Gravatar Arnaud Spiwack2014-06-06
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Gravatar Yves Bertot2014-05-06
* - Fix handling of polymorphic inductive elimination schemes.Gravatar Matthieu Sozeau2014-05-06
* - Fix Check to use the constraints inferred during type inference.Gravatar Matthieu Sozeau2014-05-06
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Adding a stm/ folder, as asked during last workgroup. It was essentially movingGravatar Pierre-Marie Pédrot2014-04-25
* Fixing various backtrace recordings.Gravatar Pierre-Marie Pédrot2014-04-25
* Add an option -Q (tentative name).Gravatar Guillaume Melquiond2014-04-08
* Adding a Print Strategy vernacular command. It allows to check theGravatar Pierre-Marie Pédrot2014-03-19
* Using Hashmaps by default in constant and inductive maps. This changes fold andGravatar Pierre-Marie Pédrot2014-03-07
* Using HMaps in Safe_env.environments, hopefully improving performances.Gravatar Pierre-Marie Pédrot2014-03-05
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* CoqIDE: print message of "Fail" commandGravatar Enrico Tassi2014-02-26
* Simpl_behaviour becomes Reductionops.ReductionBehaviourGravatar Pierre Boutillier2014-02-24
* Timeout and Set Default Timeout fixed (closes: #3229)Gravatar Enrico Tassi2014-02-10
* Removing the [Require "file"] syntax.Gravatar Pierre-Marie Pédrot2014-02-02
* Load implemented in CoqIDE/STM (closes: #3223)Gravatar Enrico Tassi2014-01-30
* Make Require verboseGravatar Pierre Boutillier2014-01-13
* Proof_using: new syntax + suggestionGravatar Enrico Tassi2014-01-05
* Notations can now accept dummy arguments. If ever a bound variable is notGravatar Pierre-Marie Pédrot2013-12-22
* Removing the need of evarmaps in constr internalization.Gravatar Pierre-Marie Pédrot2013-12-17
* The commands that initiate proofs are now in charge of what happens when proo...Gravatar Arnaud Spiwack2013-12-04
* Centralizing the Ltac-defining functions in Tacenv.Gravatar ppedrot2013-11-10
* Made multiple-goal tactic work after all: .Gravatar aspiwack2013-11-02
* Fixes parsing of all: followed by a typechecking/evaluation command.Gravatar aspiwack2013-11-02
* Adds a new goal selector "all:".Gravatar aspiwack2013-11-02
* The tactic [admit] exits with the "unsafe" status.Gravatar aspiwack2013-11-02
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
* Conv_orable made functional and part of pre_envGravatar gareuselesinge2013-10-31
* cList: a few alternative to hashtbl-based uniquize, distinct, subsetGravatar letouzey2013-10-23
* cList: set-as-list functions are now with an explicit comparisonGravatar letouzey2013-10-23
* declaration_hooks use EphemeronGravatar gareuselesinge2013-10-18
* Remove some uses of local modules (some were unused, some were costly).Gravatar xclerc2013-10-14
* STM: fix verbosity of queriesGravatar gareuselesinge2013-10-07
* Moving side effects into evar_map. There was no reason to keep anotherGravatar ppedrot2013-10-05
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
* get rid of closures in global/proof stateGravatar gareuselesinge2013-08-08
* Support Proof GeneralGravatar gareuselesinge2013-08-08
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Replacing uses of association lists by maps in notations.Gravatar ppedrot2013-08-03
* Added a Print Debug GC command that displays the current state ofGravatar ppedrot2013-08-01