aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-04-10comments: corrected in the Context moduleMatej Kosik
2017-04-10trivialMatej Kosik
2017-04-10trivialMatej Kosik
2017-04-10simplify: Environ.push_namedMatej Kosik
2017-04-10refactoring: Names.DirPath.is_emptyMatej Kosik
2017-04-10refactoring: Names.DirPath.compareMatej Kosik
2017-04-10refactoring: Names.DirPath.equalMatej Kosik
2017-04-10comment: typoMatej Kosik
2017-04-10refactoring: Reductionops.contextual_reduction_function typeMatej Kosik
2017-04-10Merge PR#547: [toplevel] Remove the feedback printer only on exit.Maxime Dénès
2017-04-10Merge PR#548: [ide] Correctly place warning tags.Maxime Dénès
2017-04-09Merge PR#460: Turning the printing primitive projection compatibility flag of...Maxime Dénès
2017-04-08[ide] Correctly place warning tags.Emilio Jesus Gallego Arias
2017-04-08Update the .mailmap file.Guillaume Melquiond
2017-04-07Merge PR#461: [camlpX] Remove camlp4 compat layer.Maxime Dénès
2017-04-07[toplevel] Remove the feedback feeder printing only on exit.Emilio Jesus Gallego Arias
2017-04-07Fixes for Drop. to work (decl_mode removal and toplevel -> vernac)Matthieu Sozeau
2017-04-07Merge PR#485: Document Show MatchMaxime Dénès
2017-04-07Remove a forgotten rule for decl_mode from the Makefile.Pierre-Marie Pédrot
2017-04-07Turning the printing primitive projection parameter flag off by default.Hugo Herbelin
2017-04-07Turning the printing primitive projection compatibility flag off by default.Hugo Herbelin
2017-04-07[travis] Overlay for PR#461: Camlp4 removal.Emilio Jesus Gallego Arias
2017-04-07[camlpX] Enrico's changes to camlp4 removal.Emilio Jesus Gallego Arias
2017-04-07[camlpX] Remove camlp4 compat layer.Emilio Jesus Gallego Arias
2017-04-07Merge PR#530: [toplevel] Remove exception error printer in favor of feedback ...Maxime Dénès
2017-04-07Merge PR#519: Faster side effectsMaxime Dénès
2017-04-07Inline the only use of hcons_j in Term_typing.Pierre-Marie Pédrot
2017-04-06Merge PR#455: Farewell decl_modeMaxime Dénès
2017-04-06Merge PR#488: Adding a documentation for the new proof engine.Maxime Dénès
2017-04-06Adding a documentation for the new proof engine.Pierre-Marie Pédrot
2017-04-06Documenting the fact terms are only hashconsed outside of a section.Pierre-Marie Pédrot
2017-04-06Merge PR#508: Optimize pending evarsMaxime Dénès
2017-04-06Merge PR#542: [travis] Add webhook to Gitter.Maxime Dénès
2017-04-06[travis] Add webhook to Gitter.Théo Zimmermann
2017-04-05[toplevel] Remove exception error printer in favor of feedback printer.Emilio Jesus Gallego Arias
2017-04-05Merge PR#434: Optimizing array mapping in the kernel.Maxime Dénès
2017-04-04Merge PR#502: [pp] Add anomaly header to error messages.Maxime Dénès
2017-04-03Merge branch 'v8.6' into trunkMaxime Dénès
2017-04-03Merge PR#533: Instances should obey universe binders even when defined by tac...Maxime Dénès
2017-04-03Fix loading of ocamldebug printers.Pierre-Marie Pédrot
2017-04-03Instances should obey universe binders even when defined by tactics.Gaetan Gilbert
2017-04-03Merge PR#417: No cast surgery in let inMaxime Dénès
2017-04-03Add test file for #4957.Maxime Dénès
2017-04-02Fix higher-order pattern variables not being printed as "@?" (bug #5431).Guillaume Melquiond
2017-04-02Fix documentation typo (bug #5433).Guillaume Melquiond
2017-04-02Simplify some proofs.Guillaume Melquiond
2017-04-01Declaring ltac plugin, so that static linking works.Hugo Herbelin
2017-03-30Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-30Merge PR#463: Run non-tactic comands without resilient_commandMaxime Dénès
2017-03-30Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R.Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-23 03:18:09 +0000