aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernacentries.ml
Commit message (Expand)AuthorAge
* Notation: option to attach extra pretty printing rules to notationsGravatar Enrico Tassi2014-09-29
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
* Rework typeclass resolution and control of backtracking.Gravatar Matthieu Sozeau2014-09-15
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Commands like [Inductive > X := … | … | …] raise an error message inste...Gravatar Arnaud Spiwack2014-09-04
* Remove [Infer] option of records.Gravatar Arnaud Spiwack2014-09-04
* Type definitions [Variant] and [Record] really don't accept the wrong kind of...Gravatar Arnaud Spiwack2014-09-04
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
* Moving code of tactic interpretation from Tacenv to Vernacentries.Gravatar Pierre-Marie Pédrot2014-08-31
* Fixing the essence of naming bug #3204: use same strategy for namingGravatar Hugo Herbelin2014-08-25
* STM: new "par:" goal selector, like "all:" but in parallelGravatar Enrico Tassi2014-08-05
* Unifying locate code, also making it more powerful: it is now able to findGravatar Pierre-Marie Pédrot2014-07-21
* Adding a new "Locate Term" command, distinct from the raw "Locate" command.Gravatar Pierre-Marie Pédrot2014-07-21
* More complete printing of Ltac location, akin to the term-dedicated Locate co...Gravatar Pierre-Marie Pédrot2014-07-21
* smartlocate: look for the head symbol for realGravatar Enrico Tassi2014-07-14
* Adding a "time" tactical for benchmarking purposes. In case the tacticGravatar Hugo Herbelin2014-07-13
* Revert "time tac" (committed by mistake).Gravatar Hugo Herbelin2014-07-07
* time tacGravatar Hugo Herbelin2014-07-07
* Add toplevel commands to declare global universes and constraints.Gravatar Matthieu Sozeau2014-07-01
* all coqide specific files moved into ide/Gravatar Enrico Tassi2014-06-25
* Proper handling of the polymorphism flag for Context, fixing HoTT bug #98.Gravatar Matthieu Sozeau2014-06-23
* - 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 13:53:26 +0000