| Age | Commit message (Expand) | Author |
|---|
| 2017-05-31 | Merge PR#560: Reinstate fixpoint refolding in [cbn], deactivated by mistake (... | Maxime Dénès |
| 2017-05-31 | Tests for new specialize feature + CHANGES. | Pierre Courtieu |
| 2017-05-31 | Documenting the new behaviour of specialize. | Pierre Courtieu |
| 2017-05-31 | Make specialize smarter. | Pierre Courtieu |
| 2017-05-31 | Merge PR#700: make sure that "ocamllibdep" properly recognizes Ocaml that are... | Maxime Dénès |
| 2017-05-31 | Merge PR#699: Fix bug 5550: "typeclasses eauto with" does not work with secti... | Maxime Dénès |
| 2017-05-31 | removing duplicate line from "tools/CoqMakefile.in" | Matej Košík |
| 2017-05-31 | Adding overlay for math-comp. | Hugo Herbelin |
| 2017-05-31 | Using a more explicit algebraic type for evars of kind "MatchingVar". | Hugo Herbelin |
| 2017-05-31 | Renaming allow_patvar flag of intern_gen into pattern_mode. | Hugo Herbelin |
| 2017-05-31 | Overlay for math-comp. | Hugo Herbelin |
| 2017-05-31 | Factorizing interp_gen through a function interpreting glob_constr. | Hugo Herbelin |
| 2017-05-31 | Splitting interp_open_constr into two variants, with or without type classes. | Hugo Herbelin |
| 2017-05-31 | Creating a module Nameops.Name extending module Names.Name. | Hugo Herbelin |
| 2017-05-31 | Renaming interp_rawcontext_evars using a more "standard" name. | Hugo Herbelin |
| 2017-05-31 | Locating error about clash between a inductive parameter and a bound variable. | Hugo Herbelin |
| 2017-05-31 | More precise on preventing clash between bound vars name and hidden impargs. | Hugo Herbelin |
| 2017-05-31 | Fixing #5233 (missing implicit arguments for recursive records). | Hugo Herbelin |
| 2017-05-31 | Fixing a failure to interpret some local implicit arguments in Inductive. | Hugo Herbelin |
| 2017-05-31 | Using EConstr and more invariants in record.ml. | Hugo Herbelin |
| 2017-05-31 | Fixing #5523 (missing support for complex constructions in recursive notations). | Hugo Herbelin |
| 2017-05-31 | Fixing a too lax constraint for finding recursive binder part of a notation. | Hugo Herbelin |
| 2017-05-30 | [ide] Correct merging error. | Emilio Jesus Gallego Arias |
| 2017-05-30 | Merge PR#706: Add some test-suite generated files to .gitignore | Maxime Dénès |
| 2017-05-30 | coq_makefile : do not build bytecode versions of plugins by default | Pierre Letouzey |
| 2017-05-30 | [gitlab] Artifact test suite logs on failure. | Gaëtan Gilbert |
| 2017-05-30 | Add test-suite checks for coqchk with constraints | Jason Gross |
| 2017-05-30 | Add some test-suite generated files to .gitignore | Jason Gross |
| 2017-05-30 | Fix empty parentheses display in test-suite | Jason Gross |
| 2017-05-30 | Makefile: $(BEST) controls which coqtop is used to build .vo | Pierre Letouzey |
| 2017-05-30 | Makefile: no bytecode compilation in make world, see make byte instead | Pierre Letouzey |
| 2017-05-30 | Merge PR#693: A subtle bug in tclWITHHOLES. | Maxime Dénès |
| 2017-05-30 | [readlink -f] doesn't work on OSX | Gaëtan Gilbert |
| 2017-05-30 | Support for using type information to infer more precise evar sources. | Hugo Herbelin |
| 2017-05-30 | Merge PR#695: Omega: fix bug #4132 | Maxime Dénès |
| 2017-05-30 | Documentation for eassert, eenough, epose proof, eset, eremember, epose. | Hugo Herbelin |
| 2017-05-30 | Few tests for e-variants of assert, set, remember. | Hugo Herbelin |
| 2017-05-30 | Adding "epose", "eset", "eremember" which allow to set terms with | Hugo Herbelin |
| 2017-05-30 | Adding "eassert", "eenough", "epose proof", which allow to state | Hugo Herbelin |
| 2017-05-30 | make sure that "ocamllibdep" properly recognizes Ocaml modules that are all u... | Matej Košík |
| 2017-05-30 | Fix bug 5550: "typeclasses eauto with" does not work with section variables. | Théo Zimmermann |
| 2017-05-30 | Merge PR#356: Making management of installation directories more structured, ... | Maxime Dénès |
| 2017-05-30 | cleanup in ".merlin" file | Matej Kosik |
| 2017-05-30 | make the expansion of the "DECLARE PLUGIN" closer to the way how a human woul... | Matej Kosik |
| 2017-05-30 | Merge PR#692: Fail on deprecated warning even for Ocaml > 4.02.3 | Maxime Dénès |
| 2017-05-29 | Merge PR#687: Gitlab CI | Maxime Dénès |
| 2017-05-29 | Pretyping cleanup: remove constr_of_global calls | Matthieu Sozeau |
| 2017-05-29 | tactics cleanup: remove constr_of_global calls | Matthieu Sozeau |
| 2017-05-29 | Omega: use "simpl" only on coefficents, not on atoms (fix #4132) | Pierre Letouzey |
| 2017-05-29 | Merge PR#690: [stm] Uniformize `Sideff / Sideff. | Maxime Dénès |
