aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Fixing unsetting of CoqIDE tags.Gravatar Pierre-Marie Pédrot2015-09-24
* Fixing fake_ide.Gravatar Pierre-Marie Pédrot2015-09-22
* Rich printing of CoqIDE protocol failure.Gravatar Pierre-Marie Pédrot2015-09-20
* Rich printing of messages.Gravatar Pierre-Marie Pédrot2015-09-20
* Rich printing of goals.Gravatar Pierre-Marie Pédrot2015-09-20
* Adding rich printing primitives.Gravatar Pierre-Marie Pédrot2015-09-20
* Do not canonicalize messages received by CoqIDE.Gravatar Pierre-Marie Pédrot2015-09-20
* Pluging in tag preferences into buffer printing.Gravatar Pierre-Marie Pédrot2015-09-20
* Adding standard printing tags to CoqIDE.Gravatar Pierre-Marie Pédrot2015-09-20
* Adding a tag preferenceGravatar Pierre-Marie Pédrot2015-09-20
* Better debug printers for module paths.Gravatar Maxime Dénès2015-09-20
* Fix previous merge.Gravatar Maxime Dénès2015-09-17
* Merge branch 'v8.5' into trunkGravatar Maxime Dénès2015-09-17
|\
| * 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
* | Remove dead code in lazy reduction machine.Gravatar Maxime Dénès2015-09-14
* | Coq_makefile: read TIMED and TIMECMD from environment.Gravatar Maxime Dénès2015-09-13
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-09-13
|\|
| * Fixing bug #2498: Coqide navigation preferences delayed effect.Gravatar Pierre-Marie Pédrot2015-09-12
| * typo in refman.Gravatar Pierre Courtieu2015-09-10
* | Assertion checking that invariant enforced by 0f8d1b92 always holds.Gravatar Maxime Dénès2015-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
* | Merge remote-tracking branch 'origin/v8.5' into trunkGravatar Hugo Herbelin2015-09-09
|\|
| * 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
* | Documenting the new behaviour of the Shrink Obligations flag.Gravatar Pierre-Marie Pédrot2015-09-08
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 01:08:15 +0000