aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* Univs: fix handling of evar_map in identity coercion construction.Gravatar Matthieu Sozeau2015-10-05
* Fix after rebase...Gravatar Matthieu Sozeau2015-10-02
* Univs: fix inference of the lowest sort for records.Gravatar Matthieu Sozeau2015-10-02
* Univs: correcly compute the levels of records when they fall in Prop.Gravatar Matthieu Sozeau2015-10-02
* Univs/program: handle side effects in obligations.Gravatar Matthieu Sozeau2015-10-02
* Univs: fix Show Universes.Gravatar Matthieu Sozeau2015-10-02
* Univs: fix environment handling in scheme building.Gravatar Matthieu Sozeau2015-10-02
* Univs: fix after rebase (from_ctx/from_env)Gravatar Matthieu Sozeau2015-10-02
* Univs: fix many evar_map initializations and leaks.Gravatar Matthieu Sozeau2015-10-02
* Universes: enforce Set <= i for all Type occurrences.Gravatar Matthieu Sozeau2015-10-02
* Prevent States.intern_state and System.extern_intern from looking up files in...Gravatar Guillaume Melquiond2015-09-29
* Remove some uses of Loadpath.get_paths.Gravatar Guillaume Melquiond2015-09-29
* Make -load-vernac-object respect the loadpath.Gravatar Guillaume Melquiond2015-09-28
* The -require option now accepts a logical path instead of a physical one.Gravatar Pierre-Marie Pédrot2015-09-25
* Updating the documentation and the toolchain w.r.t. the change in -compile.Gravatar Pierre-Marie Pédrot2015-09-25
* The -compile option now accepts ".v" files and outputs a warning otherwise.Gravatar Pierre-Marie Pédrot2015-09-25
* Hopefully better names to constructors of internal_flag, as discussedGravatar Hugo Herbelin2015-09-23
* Give a way to control if the decidable-equality schemes are built likeGravatar Hugo Herbelin2015-09-23
* Removing the generalization of the body of inductive schemes fromGravatar Hugo Herbelin2015-09-23
* Fix #3948 Anomaly: unknown constant in Print AssumptionsGravatar Maxime Dénès2015-09-20
* Fixing bug #4269: [Print Assumptions] lies about which axioms a term depends on.Gravatar Pierre-Marie Pédrot2015-09-15
* Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
* Also there's an extra space in the error message.Gravatar mlasson2015-09-03
* Code cleaning in Obligations.Gravatar Pierre-Marie Pédrot2015-08-22
* Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
* Give a way to control if the decidable-equality schemes are built likeGravatar Hugo Herbelin2015-08-02
* Removing the generalization of the body of inductive schemes fromGravatar Hugo Herbelin2015-08-02
* For convenience, making yes and on, and no and off synonymous inGravatar Hugo Herbelin2015-08-02
* Use open_utf8_file_in for opening files in the IDE. (Fix bug #2874)Gravatar Guillaume Melquiond2015-07-28
* Improving over 26aa224293 in reporting unexpected error during scheme creation.Gravatar Hugo Herbelin2015-07-27
* Fixing bug #3736 (anomaly instead of error/warning/silence onGravatar Hugo Herbelin2015-07-27
* Option -type-in-type: added support in checker and making it contaminatingGravatar Hugo Herbelin2015-07-10
* Fixing "Load" without "Verbose" in coqtop, after vernac_com lost itsGravatar Hugo Herbelin2015-07-07
* Fix loop in assumptions (Close: #4275)Gravatar Enrico Tassi2015-07-02
* Assumptions: more informative print for False axiom (Close: #4054)Gravatar Enrico Tassi2015-06-29
* Reinstall Set Printing Universes option overwritten by Maxime!Gravatar Matthieu Sozeau2015-06-28
* Fix bug #4254 with the help of J.H. JourdanGravatar Matthieu Sozeau2015-06-26
* Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Gravatar Lionel Rieg2015-06-26
* Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Gravatar Thomas Sibut-Pinote2015-06-25
* improve --help documentation: the -m|--memory option was missingGravatar Gabriel Scherer2015-06-24
* when OCAML_GC_STATS points to a filepath, write Gc stats into itGravatar Gabriel Scherer2015-06-24
* Splitting the library representation on disk in two.Gravatar Pierre-Marie Pédrot2015-06-24
* obligations: wrap Ephemeron.get to make error more informativeGravatar Enrico Tassi2015-06-23
* Wrap the program_info type up in the ephemeron mechanismGravatar Alec Faithfull2015-06-23
* Add a Set Dump Bytecode command for debugging purposes.Gravatar Maxime Dénès2015-06-23
* Warning are enabled by default in interactive mode.Gravatar Pierre-Marie Pédrot2015-06-23
* Remove uses of polymorphic equality from prev. commitGravatar Clément Pit--Claudel2015-06-22
* Replace 'try ... with Failure "List.last"' with 'if l <> []'Gravatar Clément Pit--Claudel2015-06-22
* Guard the List.hd call in [Show Intros]Gravatar Clément Pit--Claudel2015-06-22
* coqtop: reset the current file name after a load-vernac-sourceGravatar Enrico Tassi2015-05-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 20:28:24 +0000