aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-06-09newring: fix for hack using evars as integers.Matthieu Sozeau
2016-06-09Adding a bit of documentation in the mli.Pierre-Marie Pédrot
2016-06-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-06-09Fixing #4644 (regression of unification on evar-evar problems with a match).Hugo Herbelin
2016-06-09Minor simplification in evarconv.ml.Hugo Herbelin
2016-06-09New update on how to find camlp5 binary and library at configure time.Hugo Herbelin
2016-06-09Improve the interpretation scope of arguments of an ltac match.Hugo Herbelin
2016-06-09Reverting dbdff037 which does not seem to prevent to have #3638 fixedHugo Herbelin
2016-06-09Documenting API changes in dev/doc/changes.txt.Pierre-Marie Pédrot
2016-06-09Merge PR #190: Add configurable shortcuts for user queries to CoqIDE.Pierre-Marie Pédrot
2016-06-09Merge PR #197.Pierre-Marie Pédrot
2016-06-09Remove failure on non-.v files (bug #4752).Guillaume Melquiond
2016-06-08Adding profiling developer information in dev/doc/profiling.txt.Pierre-Marie Pédrot
2016-06-08Add an explicit replacement rule for Refine moduleJason Gross
2016-06-08coq_makefile: fix a crucial typo in e9c57a3Pierre Letouzey
2016-06-08remove grammar/grammar.mllibPierre Letouzey
2016-06-08Merge branch 'divided-makefile' into trunkPierre Letouzey
2016-06-08Makefile.build split in many smaller files : Makefile.{ide,checker,dev,install}Pierre Letouzey
2016-06-08Makefile: avoid overwriting test.ml when testing grammar.cmaPierre Letouzey
2016-06-08Makefile: make clean now removes the .coq-native subdirsPierre Letouzey
2016-06-08Officially discontinue the experimental coq build via ocamlbuildPierre Letouzey
2016-06-08proofs/proofs.mllib: no more proof_errors !Pierre Letouzey
2016-06-07Search interface revisions.Pierre-Marie Pédrot
2016-06-07Removing the convenience functions from the Search API.Pierre-Marie Pédrot
2016-06-07Fix bug #4777: Printing time is impacted by large terms that don't print.Pierre-Marie Pédrot
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-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-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-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-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-03-23 02:29:31 +0000