aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-06-13Fix test-suite file, only part 2 is fixed in 8.5Matthieu Sozeau
2016-06-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-06-13Univs: fix for part #2 of bug #4816.Matthieu Sozeau
2016-06-13STM classification: VernacTimeout may contain an "internal command".Maxime Dénès
2016-06-13Print Assumptions and co. can "pierce opacity".Maxime Dénès
2016-06-13evar_conv: Refine occur_rigidlyMatthieu Sozeau
2016-06-13Tentatively fixing misguiding error message with "binder" type inHugo Herbelin
2016-06-12For the record, an example one would like to see working.Hugo Herbelin
2016-06-12Minor simplification in evarconv.Hugo Herbelin
2016-06-12Another fix to #4782 (a typing error not captured when dealing with bindings).Hugo Herbelin
2016-06-12Reserve exception "ConversionFailed" in unification for failure ofHugo Herbelin
2016-06-12Protecting eta-expansion in evarconv.ml against ill-typed problems.Hugo Herbelin
2016-06-12Fixing bug in printing CannotSolveConstraint (collision of context names).Hugo Herbelin
2016-06-11Fixing #4782 (a typing error not captured when dealing with bindings).Hugo Herbelin
2016-06-11Fixing a try with in apply that has become too weak in 8.5.Hugo Herbelin
2016-06-10Merge branch 'pack-plugins'Pierre Letouzey
2016-06-10coq_makefile: oups, a missing ; in my previous commitPierre Letouzey
2016-06-10coq_makefile: fix a crucial typo in e9c57a3Pierre Letouzey
2016-06-10coq_makefile: short display of COQC and COQDEP (follow-up of e9c57a3)Pierre Letouzey
2016-06-10A mini-optimization for free in unification.ml: test in O(1)Hugo Herbelin
2016-06-09Reporting about a few bug fixes (to be continued).Hugo Herbelin
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-09Unbreak singleton list-like notation (-compat 8.4)Jason Gross
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-09Univs/(e)auto: fix bug #4450 polymorphic exact hintsMatthieu Sozeau
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-08Compilation via pack for plugins of the stdlibPierre 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-07Add is_ind, is_constructor, is_projJason Gross
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 18:51:09 +0000