aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-09-29Make the interface of System.raw_extern_intern much saner.Guillaume Melquiond
2015-09-29Prevent States.intern_state and System.extern_intern from looking up files in...Guillaume Melquiond
2015-09-29Remove some uses of Loadpath.get_paths.Guillaume Melquiond
2015-09-28Make -load-vernac-object respect the loadpath.Guillaume Melquiond
2015-09-27Fixing loss of extra data in Evd.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-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-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-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-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-18Do not compress match constructs when the inner match contains no branch. (Fi...Guillaume Melquiond
2015-09-17Revert changes in Makefile.build done as part of 2bc88f9a.Maxime Dénès
2015-09-17Fix Windows installer.Guillaume Melquiond
2015-09-16In pat/constr introduction patterns, fixing in a better way clearing problemsHugo Herbelin
2015-09-16Explain new flags for native_compute in CHANGES.Maxime Dénès
2015-09-16Disable native_compute on Windows by default.Maxime Dénès
2015-09-16In configure: -no-native-compiler -> -native-compiler noMaxime Dénès
2015-09-16Continuing investigation on how to preserve the locality of the actionHugo Herbelin
2015-09-16Change coq_makefile's default from "-Q . Top" to "-R . Top". (Fix bug #3603)Guillaume Melquiond
2015-09-16Properly handle {|...|} patterns when patterns are not asymmetric. (Fix bug #...Guillaume Melquiond
2015-09-15Removing a warning in CoqOps.Pierre-Marie Pédrot
2015-09-15Test for bug #4269.Pierre-Marie Pédrot
2015-09-15Fixing bug #4269: [Print Assumptions] lies about which axioms a term depends on.Pierre-Marie Pédrot
2015-09-15STM: Reset takes Ltac <ident> into account (Close #4316)Enrico Tassi
2015-09-14Univs: Add universe binding lists to definitionsMatthieu Sozeau
2015-09-12Fixing bug #2498: Coqide navigation preferences delayed effect.Pierre-Marie Pédrot
2015-09-10typo in refman.Pierre Courtieu
2015-09-10Fixing previous patch.Pierre-Marie Pédrot
2015-09-10Fixing the XML lexer definition of names to match the standard.Pierre-Marie Pédrot
2015-09-10Extending the grammar for CoqIDE preferences so as to match trunk.Pierre-Marie Pédrot
2015-09-08Emphasizing that eta for vectors is an instance of caseS, as pointedHugo Herbelin
2015-09-08Fixing incomplete bugfix in 76f27140e6e34 (unfortunately 5 commitsHugo Herbelin
2015-09-08Minor modifications to WeakFanTheorem.Hugo Herbelin
2015-09-08Ensuring that patterns of the form pat/constr move the hypotheses replacingHugo Herbelin
2015-09-08Short cosmetic changes in tactics.ml.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 16:52:40 +0000