aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-09-17Fix previous merge.Maxime Dénès
2015-09-17Merge branch 'v8.5' into trunkMaxime Dénès
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-14Remove dead code in lazy reduction machine.Maxime Dénès
2015-09-13Coq_makefile: read TIMED and TIMECMD from environment.Maxime Dénès
2015-09-13Merge branch 'v8.5'Pierre-Marie Pédrot
2015-09-12Fixing bug #2498: Coqide navigation preferences delayed effect.Pierre-Marie Pédrot
2015-09-10typo in refman.Pierre Courtieu
2015-09-10Assertion checking that invariant enforced by 0f8d1b92 always holds.Maxime Dénès
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-09Merge remote-tracking branch 'origin/v8.5' into trunkHugo Herbelin
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
2015-09-08A bit of documentation of OCaml code for intro_patterns.Hugo Herbelin
2015-09-08New option "Unset Bracketing Last Introduction Pattern" for preservingHugo Herbelin
2015-09-08Fixing clearing of temporary hypotheses with intro pattern pat/constr.Hugo Herbelin
2015-09-08Fixing "pose proof (H ...) as H" and "assert (H:=H ...) which were supposedHugo Herbelin
2015-09-08Hacking parser so as to support both [> ... ] and [id].Hugo Herbelin
2015-09-08Adding a proof of eta on Vector.t of non-zero size.Hugo Herbelin
2015-09-08Documenting the code when preference is given to expansion of defaultHugo Herbelin
2015-09-08Documenting the new behaviour of the Shrink Obligations flag.Pierre-Marie Pédrot
2015-09-08All Program obligations now respect the Shrink Obligation flag.Pierre-Marie Pédrot
2015-09-08More potentialities in proof_terminators.Pierre-Marie Pédrot
2015-09-08Opacifying the proof_terminator type.Pierre-Marie Pédrot
2015-09-08Fixing the Shrink Obligations option.Pierre-Marie Pédrot
2015-09-06Merge branch 'v8.5' into trunkMaxime Dénès
2015-09-06Output a warning when conversion compilation failed.Maxime Dénès
2015-09-06Fix a bug in 31 bit arithmetic, leading to failing conversion tests.Maxime Dénès
2015-09-06Fixed critical bug in 31 bit arithmetic of VMCatalin Hritcu
2015-09-06Merge branch 'v8.5'Pierre-Marie Pédrot
2015-09-06Adding a Makefile target for the MSets and MMaps directories.Pierre-Marie Pédrot
2015-09-03Update test-suite after 518049fe7.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 01:42:14 +0000