aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2015-10-02Univs/program: handle side effects in obligations.Matthieu Sozeau
2015-10-02Univs: fix Show Universes.Matthieu Sozeau
2015-10-02Univs: fix environment handling in scheme building.Matthieu Sozeau
2015-10-02Univs: fix after rebase (from_ctx/from_env)Matthieu Sozeau
2015-10-02Univs: fix many evar_map initializations and leaks.Matthieu Sozeau
2015-10-02Universes: enforce Set <= i for all Type occurrences.Matthieu Sozeau
2015-09-29Prevent States.intern_state and System.extern_intern from looking up files in...Guillaume Melquiond
2015-09-29Remove some uses of Loadpath.get_paths.Guillaume Melquiond
2015-09-28Make -load-vernac-object respect the loadpath.Guillaume Melquiond
2015-09-25Merge branch 'v8.5'Pierre-Marie Pédrot
2015-09-25The -require option now accepts a logical path instead of a physical one.Pierre-Marie Pédrot
2015-09-25Updating the documentation and the toolchain w.r.t. the change in -compile.Pierre-Marie Pédrot
2015-09-25The -compile option now accepts ".v" files and outputs a warning otherwise.Pierre-Marie Pédrot
2015-09-25Declare assumptions of well-founded definitions as unsafe.Arnaud Spiwack
2015-09-25Propagate `Guarded` flag from syntax to kernel.Arnaud Spiwack
2015-09-25Add a flag in `VernacFixpoint` and `VernacCoFixpoint` to control assuming gua...Arnaud Spiwack
2015-09-23Hopefully better names to constructors of internal_flag, as discussedHugo Herbelin
2015-09-23Give a way to control if the decidable-equality schemes are built likeHugo Herbelin
2015-09-23Removing the generalization of the body of inductive schemes fromHugo Herbelin
2015-09-20Fix #3948 Anomaly: unknown constant in Print AssumptionsMaxime Dénès
2015-09-17Merge branch 'v8.5' into trunkMaxime Dénès
2015-09-15Fixing bug #4269: [Print Assumptions] lies about which axioms a term depends on.Pierre-Marie Pédrot
2015-09-14Univs: Add universe binding lists to definitionsMatthieu Sozeau
2015-09-08All Program obligations now respect the Shrink Obligation flag.Pierre-Marie Pédrot
2015-09-08Fixing the Shrink Obligations option.Pierre-Marie Pédrot
2015-09-06Merge branch 'v8.5'Pierre-Marie Pédrot
2015-09-03Also there's an extra space in the error message.mlasson
2015-08-22Code cleaning in Obligations.Pierre-Marie Pédrot
2015-08-14Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080Jason Gross
2015-08-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-08-02Reverting 16 last commits, committed mistakenly using the wrong push command.Hugo Herbelin
2015-08-02Give a way to control if the decidable-equality schemes are built likeHugo Herbelin
2015-08-02Removing the generalization of the body of inductive schemes fromHugo Herbelin
2015-08-02For convenience, making yes and on, and no and off synonymous inHugo Herbelin
2015-07-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-07-28Use open_utf8_file_in for opening files in the IDE. (Fix bug #2874)Guillaume Melquiond
2015-07-27search: Add an output-name-only search optionClément Pit--Claudel
2015-07-27Improving over 26aa224293 in reporting unexpected error during scheme creation.Hugo Herbelin
2015-07-27Fixing bug #3736 (anomaly instead of error/warning/silence onHugo Herbelin
2015-07-27Traversal of inductive defs in Print Assumptionsmlasson
2015-07-18Merge branch 'v8.5'Pierre-Marie Pédrot
2015-07-10Option -type-in-type: added support in checker and making it contaminatingHugo Herbelin
2015-07-07Fixing "Load" without "Verbose" in coqtop, after vernac_com lost itsHugo Herbelin
2015-07-02Merge branch 'v8.5' into trunkMaxime Dénès
2015-07-02Fix loop in assumptions (Close: #4275)Enrico Tassi
2015-06-29Assumptions: more informative print for False axiom (Close: #4054)Enrico Tassi
2015-06-28Merge branch 'v8.5'Pierre-Marie Pédrot
2015-06-28Reinstall Set Printing Universes option overwritten by Maxime!Matthieu Sozeau
2015-06-26Fix bug #4254 with the help of J.H. JourdanMatthieu Sozeau
2015-06-26Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Lionel Rieg
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-03 12:35:30 +0000