aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-07Fix an unhandled exception in Omega.Pierre-Marie Pédrot
2017-04-07Better support for printing constructors with let-ins.Hugo Herbelin
2017-04-07Fixing #4499 (not using unnamed record field in {| |} notation).Hugo Herbelin
2017-04-07Fixes for Drop. to work (decl_mode removal and toplevel -> vernac)Matthieu Sozeau
2017-04-07Add some hints to the "real" database to automatically discharge literal comp...Guillaume Melquiond
2017-04-07Merge PR#485: Document Show MatchMaxime Dénès
2017-04-07Merge branch 'master' into econstrPierre-Marie Pédrot
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-06Fix a normalization hotspot in computation of constr keys.Pierre-Marie Pédrot
2017-04-06Factor interp_instance out of Pretyping.pretype_globalGaetan Gilbert
2017-04-06Avoid strange shadowing of Pretyping.interp_universe_level_nameGaetan Gilbert
2017-04-06Fix a few programming pearls related to Time, Fail and Redirect.Maxime 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-06Merge branch 'origin/v8.5' into v8.6.Hugo Herbelin
2017-04-05[toplevel] Remove exception error printer in favor of feedback printer.Emilio Jesus Gallego Arias
2017-04-05Removing a normalization hotspot from EConstr.Pierre-Marie Pédrot
2017-04-05Fixing #5454 (an assert false with 'pat).Hugo Herbelin
2017-04-05Merge PR#434: Optimizing array mapping in the kernel.Maxime Dénès
2017-04-04closing bug file for #4306Julien Forest
2017-04-04end of correction of bug 4306Julien Forest
2017-04-04Bad correction in previous commitJulien Forest
2017-04-04Solving first problem in bug #4306. TO DO : solve the let in problemJulien Forest
2017-04-04bug file for 4306Julien Forest
2017-04-04Adding tests for chained abstract tactics.Pierre-Marie Pédrot
2017-04-04Fix substitution of abstracted lemmas.Pierre-Marie Pédrot
2017-04-04Merge PR#502: [pp] Add anomaly header to error messages.Maxime Dénès
2017-04-04Merge branch 'trunk' into pr379Maxime Dénès
2017-04-04Merge PR#535: Fix #5435: [Eval native_compute in] raises anomaly.Maxime Dénès
2017-04-04Test file for #5435: [Eval native_compute in] raises anomaly.Maxime Dénès
2017-04-04Fix bug #5435: [Eval native_compute in] raises anomaly.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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 22:50:11 +0000