aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-04-09Documenting how the recursive indices of a fixpoint are computed.Hugo Herbelin
2017-04-09More explicit message when a {struct x} argument refers to a local definition.Hugo Herbelin
2017-04-09Removing internal support for accepting "{struct x}" and co in "Theorem with".Hugo Herbelin
2017-04-08Update the .mailmap file.Guillaume Melquiond
2017-04-07Merge PR#461: [camlpX] Remove camlp4 compat layer.Maxime Dénès
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-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
2017-03-30Merge PR#469: Added take to VectorDefMaxime Dénès
2017-03-30Added take to VectorDef.George Stelle
2017-03-30Merge PR#511: [stm] Remove some obsolete vernacs/classification.Maxime Dénès
2017-03-29Merge PR#522: [coqide] Protect against size_allocate race in proofview.Maxime Dénès
2017-03-29Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-29Merge PR#514: [travis] Backport from trunk: VSTMaxime Dénès
2017-03-29Merge PR#506: [nit] Fix a couple incorrect uses of msg_error.Maxime Dénès
2017-03-29Merge PR#521: Do so that "About" tells if a reference is a coercion.Maxime Dénès
2017-03-29Merge PR#525: [ide] Fix typo in pp serialization.Maxime Dénès
2017-03-29Run non-tactic comands without resilient_commandTej Chajed
2017-03-29[ide] Fix typo in pp serialization.Emilio Jesus Gallego Arias
2017-03-28Fixing missing PropFacts.v in Logic/vo.itarget.Hugo Herbelin
2017-03-28[coqide] Protect against size_allocate race in proofview.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 17:33:34 +0000