coq - The formal proof system

Age	Commit message (Expand)	Author
2015-09-26	Use default GTK styles for CoqIDE tags.	Pierre-Marie Pédrot
2015-09-25	Merge branch 'v8.5'	Pierre-Marie Pédrot
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-24	Fixing unsetting of CoqIDE tags.	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-22	Fixing bug #4207: setoid_rewrite creates self-referring hypotheses.	Pierre-Marie Pédrot
2015-09-22	Fixing fake_ide.	Pierre-Marie Pédrot
2015-09-21	Fixing tutorial.	Pierre-Marie Pédrot
2015-09-21	Change the default modifiers for navigation. (Fix bug #4295)	Guillaume Melquiond
2015-09-20	Proof: suggest Admitted->Qed only if the proof is really complete (#4349)	Enrico Tassi
2015-09-20	Rich printing of CoqIDE protocol failure.	Pierre-Marie Pédrot
2015-09-20	Rich printing of messages.	Pierre-Marie Pédrot
2015-09-20	Rich printing of goals.	Pierre-Marie Pédrot
2015-09-20	Adding rich printing primitives.	Pierre-Marie Pédrot
2015-09-20	Do not canonicalize messages received by CoqIDE.	Pierre-Marie Pédrot
2015-09-20	Pluging in tag preferences into buffer printing.	Pierre-Marie Pédrot
2015-09-20	Adding standard printing tags to CoqIDE.	Pierre-Marie Pédrot
2015-09-20	Adding a tag preference	Pierre-Marie Pédrot
2015-09-20	Print Assumptions shows engagement.	Maxime Dénès
2015-09-20	Nametab: print debug notice only in debug mode.	Maxime Dénès
2015-09-20	Remove unused type_in_type field in safe_env.	Maxime Dénès
2015-09-20	Test file for #3948 - Anomaly: unknown constant in Print Assumptions.	Maxime Dénès
2015-09-20	Revert "On MacOS X, ensuring that files found in the file system have the"	Maxime Dénès
2015-09-20	Fix #3948 Anomaly: unknown constant in Print Assumptions	Maxime Dénès
2015-09-20	Better debug printers for module paths.	Maxime Dénès
2015-09-18	Do not compress match constructs when the inner match contains no branch. (Fi...	Guillaume Melquiond
2015-09-17	Fix previous merge.	Maxime Dénès
2015-09-17	Merge branch 'v8.5' into trunk	Maxime Dénès
2015-09-17	Revert changes in Makefile.build done as part of 2bc88f9a.	Maxime Dénès
2015-09-17	Fix Windows installer.	Guillaume Melquiond
2015-09-16	In pat/constr introduction patterns, fixing in a better way clearing problems	Hugo Herbelin
2015-09-16	Explain new flags for native_compute in CHANGES.	Maxime Dénès
2015-09-16	Disable native_compute on Windows by default.	Maxime Dénès
2015-09-16	In configure: -no-native-compiler -> -native-compiler no	Maxime Dénès
2015-09-16	Continuing investigation on how to preserve the locality of the action	Hugo Herbelin
2015-09-16	Change coq_makefile's default from "-Q . Top" to "-R . Top". (Fix bug #3603)	Guillaume Melquiond
2015-09-16	Properly handle {\|...\|} patterns when patterns are not asymmetric. (Fix bug #...	Guillaume Melquiond
2015-09-15	Removing a warning in CoqOps.	Pierre-Marie Pédrot
2015-09-15	Test for bug #4269.	Pierre-Marie Pédrot
2015-09-15	Fixing bug #4269: [Print Assumptions] lies about which axioms a term depends on.	Pierre-Marie Pédrot
2015-09-15	STM: Reset takes Ltac <ident> into account (Close #4316)	Enrico Tassi
2015-09-14	Univs: Add universe binding lists to definitions	Matthieu Sozeau
2015-09-14	Remove dead code in lazy reduction machine.	Maxime Dénès
2015-09-13	Coq_makefile: read TIMED and TIMECMD from environment.	Maxime Dénès
2015-09-13	Merge branch 'v8.5'	Pierre-Marie Pédrot
2015-09-12	Fixing bug #2498: Coqide navigation preferences delayed effect.	Pierre-Marie Pédrot