aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-09-29Remove some uses of Loadpath.get_paths.Guillaume Melquiond
2015-09-28Make -load-vernac-object respect the loadpath.Guillaume Melquiond
2015-09-27Removing meta_with_name from Evd.Pierre-Marie Pédrot
2015-09-27Removing subst_defined_metas_evars from Evd.Pierre-Marie Pédrot
2015-09-27Fixing loss of extra data in Evd.Pierre-Marie Pédrot
2015-09-27Removing uselessly duplicated function in Evd.Pierre-Marie Pédrot
2015-09-26Hardening the API of evarmaps.Pierre-Marie Pédrot
2015-09-26Use default GTK styles for CoqIDE tags.Pierre-Marie Pédrot
2015-09-26Documenting how to support some special unicode characters in coqdocHugo Herbelin
2015-09-26Clarifying the doc of coqdoc --utf8 as discussed on coq-club on August 19, 2015.Hugo Herbelin
2015-09-26Test for bug #4347.Pierre-Marie Pédrot
2015-09-26Fixing bug #4347: Not_found Exception with some Records.Pierre-Marie Pédrot
2015-09-25Show assumptions of well-foundedness in `Print Assumptions`Arnaud Spiwack
2015-09-25Add a field in `constant_body` to track constant whose well-foundedness is as...Arnaud Spiwack
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-25Prevent pretyping from checking well-guardedness unnecessarily.Arnaud Spiwack
2015-09-25Propagate `Guarded` flag from syntax to kernel.Arnaud Spiwack
2015-09-25Add (temporary) syntax for assuming guardedness in (co-)fixed points.Arnaud Spiwack
2015-09-25Add `Guarded` to the assumption tokens.Arnaud Spiwack
2015-09-25Add a flag in `VernacFixpoint` and `VernacCoFixpoint` to control assuming gua...Arnaud Spiwack
2015-09-24Fixing unsetting of CoqIDE tags.Pierre-Marie Pédrot
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-22Fixing bug #4207: setoid_rewrite creates self-referring hypotheses.Pierre-Marie Pédrot
2015-09-22Fixing fake_ide.Pierre-Marie Pédrot
2015-09-21Fixing tutorial.Pierre-Marie Pédrot
2015-09-21Change the default modifiers for navigation. (Fix bug #4295)Guillaume Melquiond
2015-09-20Proof: suggest Admitted->Qed only if the proof is really complete (#4349)Enrico Tassi
2015-09-20Rich printing of CoqIDE protocol failure.Pierre-Marie Pédrot
2015-09-20Rich printing of messages.Pierre-Marie Pédrot
2015-09-20Rich printing of goals.Pierre-Marie Pédrot
2015-09-20Adding rich printing primitives.Pierre-Marie Pédrot
2015-09-20Do not canonicalize messages received by CoqIDE.Pierre-Marie Pédrot
2015-09-20Pluging in tag preferences into buffer printing.Pierre-Marie Pédrot
2015-09-20Adding standard printing tags to CoqIDE.Pierre-Marie Pédrot
2015-09-20Adding a tag preferencePierre-Marie Pédrot
2015-09-20Print Assumptions shows engagement.Maxime Dénès
2015-09-20Nametab: print debug notice only in debug mode.Maxime Dénès
2015-09-20Remove unused type_in_type field in safe_env.Maxime Dénès
2015-09-20Test file for #3948 - Anomaly: unknown constant in Print Assumptions.Maxime Dénès
2015-09-20Revert "On MacOS X, ensuring that files found in the file system have the"Maxime Dénès
2015-09-20Fix #3948 Anomaly: unknown constant in Print AssumptionsMaxime Dénès
2015-09-20Better debug printers for module paths.Maxime Dénès
2015-09-18Do not compress match constructs when the inner match contains no branch. (Fi...Guillaume Melquiond
2015-09-17Fix previous merge.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-04 03:08:56 +0000