aboutsummaryrefslogtreecommitdiff
path: root/toplevel/vernacentries.ml
AgeCommit message (Expand)Author
2014-09-04Commands like [Inductive > X := … | … | …] raise an error message inste...Arnaud Spiwack
2014-09-04Remove [Infer] option of records.Arnaud Spiwack
2014-09-04Type definitions [Variant] and [Record] really don't accept the wrong kind of...Arnaud Spiwack
2014-09-04Print [Variant] types with the keyword [Variant].Arnaud Spiwack
2014-08-31Moving code of tactic interpretation from Tacenv to Vernacentries.Pierre-Marie Pédrot
2014-08-25Fixing the essence of naming bug #3204: use same strategy for namingHugo Herbelin
2014-08-05STM: new "par:" goal selector, like "all:" but in parallelEnrico Tassi
2014-07-21Unifying locate code, also making it more powerful: it is now able to findPierre-Marie Pédrot
2014-07-21Adding a new "Locate Term" command, distinct from the raw "Locate" command.Pierre-Marie Pédrot
2014-07-21More complete printing of Ltac location, akin to the term-dedicated Locate co...Pierre-Marie Pédrot
2014-07-14smartlocate: look for the head symbol for realEnrico Tassi
2014-07-13Adding a "time" tactical for benchmarking purposes. In case the tacticHugo Herbelin
2014-07-07Revert "time tac" (committed by mistake).Hugo Herbelin
2014-07-07time tacHugo Herbelin
2014-07-01Add toplevel commands to declare global universes and constraints.Matthieu Sozeau
2014-06-25all coqide specific files moved into ide/Enrico Tassi
2014-06-23Proper handling of the polymorphism flag for Context, fixing HoTT bug #98.Matthieu Sozeau
2014-06-16- Add "Show Universes" to print information about universes during a proof.Matthieu Sozeau
2014-06-10Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Matthieu Sozeau
2014-06-08Adding a toplevel option allowing to deactivate the term sharing in kernelPierre-Marie Pédrot
2014-06-08Moving hook code from Future to Lemmas. This seemed to disrupt compilation ofPierre-Marie Pédrot
2014-06-08Enforce a correct exception handling in declaration_hooksEnrico Tassi
2014-06-07Adding a new Control file centralizing the control options of Coq.Pierre-Marie Pédrot
2014-06-06Remove the syntax [Vernac1. Vernac2. … Vernacn. ].Arnaud Spiwack
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Adapt 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-06Initial work on reintroducing old-style polymorphism for compatibility (the s...Matthieu Sozeau
2014-05-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-25Adding a stm/ folder, as asked during last workgroup. It was essentially movingPierre-Marie Pédrot
2014-04-25Fixing various backtrace recordings.Pierre-Marie Pédrot
2014-04-08Add an option -Q (tentative name).Guillaume Melquiond
2014-03-19Adding a Print Strategy vernacular command. It allows to check thePierre-Marie Pédrot
2014-03-07Using Hashmaps by default in constant and inductive maps. This changes fold andPierre-Marie Pédrot
2014-03-05Using HMaps in Safe_env.environments, hopefully improving performances.Pierre-Marie Pédrot
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-02-26CoqIDE: print message of "Fail" commandEnrico Tassi
2014-02-24Simpl_behaviour becomes Reductionops.ReductionBehaviourPierre Boutillier
2014-02-10Timeout and Set Default Timeout fixed (closes: #3229)Enrico Tassi
2014-02-02Removing the [Require "file"] syntax.Pierre-Marie Pédrot
2014-01-30Load implemented in CoqIDE/STM (closes: #3223)Enrico Tassi
2014-01-13Make Require verbosePierre Boutillier
2014-01-05Proof_using: new syntax + suggestionEnrico Tassi
2013-12-22Notations can now accept dummy arguments. If ever a bound variable is notPierre-Marie Pédrot
2013-12-17Removing the need of evarmaps in constr internalization.Pierre-Marie Pédrot
2013-12-04The commands that initiate proofs are now in charge of what happens when proo...Arnaud Spiwack
2013-11-10Centralizing the Ltac-defining functions in Tacenv.ppedrot
2013-11-02Made multiple-goal tactic work after all: .aspiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 09:28:45 +0000