aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* 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
* Fixing bug #4207: setoid_rewrite creates self-referring hypotheses.Gravatar Pierre-Marie Pédrot2015-09-22
* Fixing tutorial.Gravatar Pierre-Marie Pédrot2015-09-21
* Change the default modifiers for navigation. (Fix bug #4295)Gravatar Guillaume Melquiond2015-09-21
* Proof: suggest Admitted->Qed only if the proof is really complete (#4349)Gravatar Enrico Tassi2015-09-20
* Print Assumptions shows engagement.Gravatar Maxime Dénès2015-09-20
* Nametab: print debug notice only in debug mode.Gravatar Maxime Dénès2015-09-20
* Remove unused type_in_type field in safe_env.Gravatar Maxime Dénès2015-09-20
* Test file for #3948 - Anomaly: unknown constant in Print Assumptions.Gravatar Maxime Dénès2015-09-20
* Revert "On MacOS X, ensuring that files found in the file system have the"Gravatar Maxime Dénès2015-09-20
* Fix #3948 Anomaly: unknown constant in Print AssumptionsGravatar Maxime Dénès2015-09-20
* Do not compress match constructs when the inner match contains no branch. (Fi...Gravatar Guillaume Melquiond2015-09-18
* Revert changes in Makefile.build done as part of 2bc88f9a.Gravatar Maxime Dénès2015-09-17
* Fix Windows installer.Gravatar Guillaume Melquiond2015-09-17
* In pat/constr introduction patterns, fixing in a better way clearing problemsGravatar Hugo Herbelin2015-09-16
* Explain new flags for native_compute in CHANGES.Gravatar Maxime Dénès2015-09-16
* Disable native_compute on Windows by default.Gravatar Maxime Dénès2015-09-16
* In configure: -no-native-compiler -> -native-compiler noGravatar Maxime Dénès2015-09-16
* Continuing investigation on how to preserve the locality of the actionGravatar Hugo Herbelin2015-09-16
* Change coq_makefile's default from "-Q . Top" to "-R . Top". (Fix bug #3603)Gravatar Guillaume Melquiond2015-09-16
* Properly handle {|...|} patterns when patterns are not asymmetric. (Fix bug #...Gravatar Guillaume Melquiond2015-09-16
* Removing a warning in CoqOps.Gravatar Pierre-Marie Pédrot2015-09-15
* Test for bug #4269.Gravatar Pierre-Marie Pédrot2015-09-15
* Fixing bug #4269: [Print Assumptions] lies about which axioms a term depends on.Gravatar Pierre-Marie Pédrot2015-09-15
* STM: Reset takes Ltac <ident> into account (Close #4316)Gravatar Enrico Tassi2015-09-15
* Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
* Fixing bug #2498: Coqide navigation preferences delayed effect.Gravatar Pierre-Marie Pédrot2015-09-12
* typo in refman.Gravatar Pierre Courtieu2015-09-10
* Fixing previous patch.Gravatar Pierre-Marie Pédrot2015-09-10
* Fixing the XML lexer definition of names to match the standard.Gravatar Pierre-Marie Pédrot2015-09-10
* Extending the grammar for CoqIDE preferences so as to match trunk.Gravatar Pierre-Marie Pédrot2015-09-10
* Emphasizing that eta for vectors is an instance of caseS, as pointedGravatar Hugo Herbelin2015-09-08
* Fixing incomplete bugfix in 76f27140e6e34 (unfortunately 5 commitsGravatar Hugo Herbelin2015-09-08
* Minor modifications to WeakFanTheorem.Gravatar Hugo Herbelin2015-09-08
* Ensuring that patterns of the form pat/constr move the hypotheses replacingGravatar Hugo Herbelin2015-09-08
* Short cosmetic changes in tactics.ml.Gravatar Hugo Herbelin2015-09-08
* A bit of documentation of OCaml code for intro_patterns.Gravatar Hugo Herbelin2015-09-08
* New option "Unset Bracketing Last Introduction Pattern" for preservingGravatar Hugo Herbelin2015-09-08
* Fixing clearing of temporary hypotheses with intro pattern pat/constr.Gravatar Hugo Herbelin2015-09-08
* Fixing "pose proof (H ...) as H" and "assert (H:=H ...) which were supposedGravatar Hugo Herbelin2015-09-08
* Hacking parser so as to support both [> ... ] and [id].Gravatar Hugo Herbelin2015-09-08
* Adding a proof of eta on Vector.t of non-zero size.Gravatar Hugo Herbelin2015-09-08
* Documenting the code when preference is given to expansion of defaultGravatar Hugo Herbelin2015-09-08
* Fix a bug in 31 bit arithmetic, leading to failing conversion tests.Gravatar Maxime Dénès2015-09-06
* Fixed critical bug in 31 bit arithmetic of VMGravatar Catalin Hritcu2015-09-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 10:45:00 +0000