aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
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
2015-06-26Add a flag to deactivate guard checking in the kernel.Arnaud Spiwack
2015-06-25Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Thomas Sibut-Pinote
2015-06-24When assuming an inductive type positive, then it is declared "unsafe" to the...Arnaud Spiwack
2015-06-24Add corresponding field in `VernacInductive`.Arnaud Spiwack
2015-06-24Add a corresponding field in `mutual_inductive_entry` (part 1).Arnaud Spiwack
2015-06-24Merge branch 'v8.5'Pierre-Marie Pédrot
2015-06-24improve --help documentation: the -m|--memory option was missingGabriel Scherer
2015-06-24when OCAML_GC_STATS points to a filepath, write Gc stats into itGabriel Scherer
2015-06-24Splitting the library representation on disk in two.Pierre-Marie Pédrot
2015-06-23obligations: wrap Ephemeron.get to make error more informativeEnrico Tassi
2015-06-23Wrap the program_info type up in the ephemeron mechanismAlec Faithfull
2015-06-23Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Thomas Sibut-Pinote
2015-06-23Add a Set Dump Bytecode command for debugging purposes.Maxime Dénès
2015-06-23Warning are enabled by default in interactive mode.Pierre-Marie Pédrot
2015-06-22Merge branch 'v8.5' into trunkPierre Letouzey
2015-06-22Remove uses of polymorphic equality from prev. commitClément Pit--Claudel
2015-06-22Replace 'try ... with Failure "List.last"' with 'if l <> []'Clément Pit--Claudel
2015-06-22Guard the List.hd call in [Show Intros]Clément Pit--Claudel
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-23 18:13:16 +0000