coq - The formal proof system

Age	Commit message (Expand)	Author
2015-10-02	Univs: fix Show Universes.	Matthieu Sozeau
2015-10-02	Univs: fix environment handling in scheme building.	Matthieu Sozeau
2015-10-02	Univs: fix after rebase (from_ctx/from_env)	Matthieu Sozeau
2015-10-02	Univs: fix many evar_map initializations and leaks.	Matthieu Sozeau
2015-10-02	Universes: enforce Set <= i for all Type occurrences.	Matthieu Sozeau
2015-09-29	Prevent States.intern_state and System.extern_intern from looking up files in...	Guillaume Melquiond
2015-09-29	Remove some uses of Loadpath.get_paths.	Guillaume Melquiond
2015-09-28	Make -load-vernac-object respect the loadpath.	Guillaume Melquiond
2015-09-25	The -require option now accepts a logical path instead of a physical one.	Pierre-Marie Pédrot
2015-09-25	Updating the documentation and the toolchain w.r.t. the change in -compile.	Pierre-Marie Pédrot
2015-09-25	The -compile option now accepts ".v" files and outputs a warning otherwise.	Pierre-Marie Pédrot
2015-09-23	Hopefully better names to constructors of internal_flag, as discussed	Hugo Herbelin
2015-09-23	Give a way to control if the decidable-equality schemes are built like	Hugo Herbelin
2015-09-23	Removing the generalization of the body of inductive schemes from	Hugo Herbelin
2015-09-20	Fix #3948 Anomaly: unknown constant in Print Assumptions	Maxime Dénès
2015-09-15	Fixing bug #4269: [Print Assumptions] lies about which axioms a term depends on.	Pierre-Marie Pédrot
2015-09-14	Univs: Add universe binding lists to definitions	Matthieu Sozeau
2015-09-03	Also there's an extra space in the error message.	mlasson
2015-08-22	Code cleaning in Obligations.	Pierre-Marie Pédrot
2015-08-02	Reverting 16 last commits, committed mistakenly using the wrong push command.	Hugo Herbelin
2015-08-02	Give a way to control if the decidable-equality schemes are built like	Hugo Herbelin
2015-08-02	Removing the generalization of the body of inductive schemes from	Hugo Herbelin
2015-08-02	For convenience, making yes and on, and no and off synonymous in	Hugo Herbelin
2015-07-28	Use open_utf8_file_in for opening files in the IDE. (Fix bug #2874)	Guillaume Melquiond
2015-07-27	Improving over 26aa224293 in reporting unexpected error during scheme creation.	Hugo Herbelin
2015-07-27	Fixing bug #3736 (anomaly instead of error/warning/silence on	Hugo Herbelin
2015-07-10	Option -type-in-type: added support in checker and making it contaminating	Hugo Herbelin
2015-07-07	Fixing "Load" without "Verbose" in coqtop, after vernac_com lost its	Hugo Herbelin
2015-07-02	Fix loop in assumptions (Close: #4275)	Enrico Tassi
2015-06-29	Assumptions: more informative print for False axiom (Close: #4054)	Enrico Tassi
2015-06-28	Reinstall Set Printing Universes option overwritten by Maxime!	Matthieu Sozeau
2015-06-26	Fix bug #4254 with the help of J.H. Jourdan	Matthieu Sozeau
2015-06-26	Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"	Lionel Rieg
2015-06-25	Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.	Thomas Sibut-Pinote
2015-06-24	improve --help documentation: the -m\|--memory option was missing	Gabriel Scherer
2015-06-24	when OCAML_GC_STATS points to a filepath, write Gc stats into it	Gabriel Scherer
2015-06-24	Splitting the library representation on disk in two.	Pierre-Marie Pédrot
2015-06-23	obligations: wrap Ephemeron.get to make error more informative	Enrico Tassi
2015-06-23	Wrap the program_info type up in the ephemeron mechanism	Alec Faithfull
2015-06-23	Add a Set Dump Bytecode command for debugging purposes.	Maxime Dénès
2015-06-23	Warning are enabled by default in interactive mode.	Pierre-Marie Pédrot
2015-06-22	Remove uses of polymorphic equality from prev. commit	Clément Pit--Claudel
2015-06-22	Replace 'try ... with Failure "List.last"' with 'if l <> []'	Clément Pit--Claudel
2015-06-22	Guard the List.hd call in [Show Intros]	Clément Pit--Claudel
2015-05-29	coqtop: reset the current file name after a load-vernac-source	Enrico Tassi
2015-05-29	Flag -test-mode intended to be used for ad-hoc prints in test-suite	Enrico Tassi
2015-05-29	make Unset Silent work in coqc	Enrico Tassi
2015-05-27	Fix bug #4159	Matthieu Sozeau
2015-05-18	Uncaught exception termination exits coqtop with the anomaly errno.	Pierre-Marie Pédrot
2015-05-18	The Fail command does not catch uncaught exception anomalies anymore.	Pierre-Marie Pédrot