aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-06-07CoqIDE: remove useless printEnrico Tassi
2016-06-07Do not use COQLIBS for the validate rule produced by coq_makefile (bug #4693).Guillaume Melquiond
2016-06-07Merge branch 'trunk' of git+ssh://scm.gforge.inria.fr/gitroot/coq/coq into trunkMatej Kosik
2016-06-07coq_makefile : minor reworkPierre Letouzey
2016-06-07Coq_makefile: code cleanup (less long lines, etc)Pierre Letouzey
2016-06-07coq_makefile: List.iteri is now standard since OCaml 4.00Pierre Letouzey
2016-06-07coq_makefile : short display of commands executed by makePierre Letouzey
2016-06-07coq_makefile: add some -ml-synonym to the ocamldep rulesPierre Letouzey
2016-06-07typoMatej Kosik
2016-06-07typographyMatej Kosik
2016-06-07printing.mllib: remove some other .mli-only from a .mllibPierre Letouzey
2016-06-07Test for #4787.Hugo Herbelin
2016-06-07Fixing #4787 (Unset Bracketing Last Introduction Pattern not working).Hugo Herbelin
2016-06-07DocumentationEnrico Tassi
2016-06-07Adding an only printing flag to notations.Pierre-Marie Pédrot
2016-06-07Removing the use to Egramcoq.recover_constr_grammar.Pierre-Marie Pédrot
2016-06-06Relying instead on the Coq85 inclusion!Hugo Herbelin
2016-06-06Mode "Bracketing Last Introduction Pattern" is on for 8.4Hugo Herbelin
2016-06-06Mode "Regular Subst Tactic" is on in 8.6.Hugo Herbelin
2016-06-06Merge remote-tracking branch 'github/pr/118' into trunkMaxime Dénès
2016-06-06Renaming: ErrorBlock -> ProofBlockEnrico Tassi
2016-06-06STM: each proof block can be enabled separatelyEnrico Tassi
2016-06-06Error box detection run only on errorEnrico Tassi
2016-06-06STM: proof block detection for indentationEnrico Tassi
2016-06-06rebase on trunkEnrico Tassi
2016-06-06STM: fix error reporting of par:Enrico Tassi
2016-06-06STM: proof block detection made optional + simple testEnrico Tassi
2016-06-06Fixing problems introduced in 8.5 with Ltac trace report. E.g.Hugo Herbelin
2016-06-06About printing of traces of failures while calling ltac code.Hugo Herbelin
2016-06-06STM: proof block detection for par:Enrico Tassi
2016-06-06STM: proof block detection for bullets and { block }Enrico Tassi
2016-06-06STM: proof block detection/error resilience APIEnrico Tassi
2016-06-06STM: carry AST and indentation of document commandsEnrico Tassi
2016-06-06STM: support for nested boxes of nodes to model error boundariesEnrico Tassi
2016-06-06STM: invalid states are first class citizensEnrico Tassi
2016-06-06xmlprotocol: fix unmarshaling of Feedback.MessageEnrico Tassi
2016-06-06xmlprotocol: uncomment marshalling code for custom messageEnrico Tassi
2016-06-06xmlprotocol: Marshal_error carries the reasonEnrico Tassi
2016-06-05Improve a comment in the test suiteJason Gross
2016-06-05Make Ltac Profiling an settingJason Gross
2016-06-05Synchronize the profiler state with the documentJason Gross
2016-06-05-profileltac -> -profile-ltac, as per @herbelinJason Gross
2016-06-05Remove a spurious tclFINALLY when not profilingJason Gross
2016-06-05Add LtacProf documentationJason Gross
2016-06-05LtacProf for Coq trunkJason Gross
2016-06-05Strip some trailing spacesJason Gross
2016-06-05Adding the Print Ltac Signatures command.Pierre-Marie Pédrot
2016-06-05Adding the Print Ltac Signature command.Pierre-Marie Pédrot
2016-06-05Remove Q_constr from grammar folder.Pierre-Marie Pédrot
2016-06-05Removing the Q_constr file.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 10:48:01 +0000