aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
| | | | | | | | | * | | | | | Makefile.build: test-suite all = run + report, so don't report againGravatar Gaëtan Gilbert2017-05-31
| | | | | | | | | * | | | | | [travis] print failing test suite logs on failureGravatar Gaëtan Gilbert2017-05-31
| | | | | | | | * | | | | | | Tests for new specialize feature + CHANGES.Gravatar Pierre Courtieu2017-05-31
| | | | | | | | * | | | | | | Documenting the new behaviour of specialize.Gravatar Pierre Courtieu2017-05-31
| | | | | | | | * | | | | | | Make specialize smarter.Gravatar Pierre Courtieu2017-05-31
* | | | | | | | | | | | | | | Merge PR#700: make sure that "ocamllibdep" properly recognizes Ocaml that are...Gravatar Maxime Dénès2017-05-31
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | |
| | | | | | | | | | | * | | | Adding overlay for math-comp.Gravatar Hugo Herbelin2017-05-31
| | | | | | | | | | | * | | | Using a more explicit algebraic type for evars of kind "MatchingVar".Gravatar Hugo Herbelin2017-05-31
| | | | | | | | | | | * | | | Renaming allow_patvar flag of intern_gen into pattern_mode.Gravatar Hugo Herbelin2017-05-31
| |_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | |
| | | | | | | | | | | | * | Overlay for math-comp.Gravatar Hugo Herbelin2017-05-31
| | | | | | | | | | | | * | Factorizing interp_gen through a function interpreting glob_constr.Gravatar Hugo Herbelin2017-05-31
| | | | | | | | | | | | * | Splitting interp_open_constr into two variants, with or without type classes.Gravatar Hugo Herbelin2017-05-31
| |_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | |
| | | | | | * | | | | | | Creating a module Nameops.Name extending module Names.Name.Gravatar Hugo Herbelin2017-05-31
| | | | | | * | | | | | | Renaming interp_rawcontext_evars using a more "standard" name.Gravatar Hugo Herbelin2017-05-31
| |_|_|_|_|/ / / / / / / |/| | | | | | | | | | |
| | | | | | | | | | | * Locating error about clash between a inductive parameter and a bound variable.Gravatar Hugo Herbelin2017-05-31
| | | | | | | | | | | * More precise on preventing clash between bound vars name and hidden impargs.Gravatar Hugo Herbelin2017-05-31
| | | | | | | | | | | * Fixing #5233 (missing implicit arguments for recursive records).Gravatar Hugo Herbelin2017-05-31
| | | | | | | | | | | * Fixing a failure to interpret some local implicit arguments in Inductive.Gravatar Hugo Herbelin2017-05-31
| | | | | | | | | | | * Using EConstr and more invariants in record.ml.Gravatar Hugo Herbelin2017-05-31
| |_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | |
| | | | | * | | | | | Fixing #5523 (missing support for complex constructions in recursive notations).Gravatar Hugo Herbelin2017-05-31
| | | | | * | | | | | Fixing a too lax constraint for finding recursive binder part of a notation.Gravatar Hugo Herbelin2017-05-31
| |_|_|_|/ / / / / / |/| | | | | | | | |
| | | | | | | | * | [ide] Correct merging error.Gravatar Emilio Jesus Gallego Arias2017-05-30
* | | | | | | | | | Merge PR#706: Add some test-suite generated files to .gitignoreGravatar Maxime Dénès2017-05-30
|\ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ / |/| | | | | | | | |
| | | | | | | | * | [gitlab] Artifact test suite logs on failure.Gravatar Gaëtan Gilbert2017-05-30
| |_|_|_|_|_|_|/ / |/| | | | | | | |
| * | | | | | | | Add some test-suite generated files to .gitignoreGravatar Jason Gross2017-05-30
|/ / / / / / / /
| | | | * / / / Fix empty parentheses display in test-suiteGravatar Jason Gross2017-05-30
| |_|_|/ / / / |/| | | | | |
| | | * | | | [readlink -f] doesn't work on OSXGravatar Gaëtan Gilbert2017-05-30
| |_|/ / / / |/| | | | |
| | * | | | Support for using type information to infer more precise evar sources.Gravatar Hugo Herbelin2017-05-30
| | * | | | Documentation for eassert, eenough, epose proof, eset, eremember, epose.Gravatar Hugo Herbelin2017-05-30
| | * | | | Few tests for e-variants of assert, set, remember.Gravatar Hugo Herbelin2017-05-30
| | * | | | Adding "epose", "eset", "eremember" which allow to set terms withGravatar Hugo Herbelin2017-05-30
| | * | | | Adding "eassert", "eenough", "epose proof", which allow to stateGravatar Hugo Herbelin2017-05-30
| |/ / / / |/| | | |
| * | | | make sure that "ocamllibdep" properly recognizes Ocaml modules that are all u...Gravatar Matej Košík2017-05-30
|/ / / /
* | | | Merge PR#356: Making management of installation directories more structured, ...Gravatar Maxime Dénès2017-05-30
|\ \ \ \
* \ \ \ \ Merge PR#692: Fail on deprecated warning even for Ocaml > 4.02.3Gravatar Maxime Dénès2017-05-30
|\ \ \ \ \
* \ \ \ \ \ Merge PR#687: Gitlab CIGravatar Maxime Dénès2017-05-29
|\ \ \ \ \ \
| | | | * | | Pretyping cleanup: remove constr_of_global callsGravatar Matthieu Sozeau2017-05-29
| | | | * | | tactics cleanup: remove constr_of_global callsGravatar Matthieu Sozeau2017-05-29
* | | | | | | Merge PR#690: [stm] Uniformize `Sideff / Sideff.Gravatar Maxime Dénès2017-05-29
|\ \ \ \ \ \ \
| | | | | * | | Ltac cleanup: no more constr_of_global callsGravatar Matthieu Sozeau2017-05-29
| | | | | * | | Equality cleanup: remove constr_of_globalGravatar Matthieu Sozeau2017-05-29
| | | | | * | | Command.ml cleanup: remove constr_of_global callsGravatar Matthieu Sozeau2017-05-29
* | | | | | | | Merge PR#555: Missing optimization when Kernel Term Sharing is disabled.Gravatar Maxime Dénès2017-05-29
|\ \ \ \ \ \ \ \
| | | | | * | | | Configuration with -local definitively seen as an installation layout like ot...Gravatar Hugo Herbelin2017-05-29
| | | | | * | | | Using the same strategy in coqdoc than in coqtop to guess the coqlib.Gravatar Hugo Herbelin2017-05-29
| | | | | * | | | Relying on computation done in Envars to discover the installation directories.Gravatar Hugo Herbelin2017-05-29
| | | | | * | | | Generalizing to docdir and datadir the test for a relocated installation.Gravatar Hugo Herbelin2017-05-29
| | | | | * | | | Exporting the suffixes needed to build coqlib, docdir, etc.Gravatar Hugo Herbelin2017-05-29
| | | | | * | | | Using Coq_config.local rather than None to tell that Coq_config.coqlib is local.Gravatar Hugo Herbelin2017-05-29
| | | | | | * | | Cleanup: removal of constr_of_global.Gravatar Matthieu Sozeau2017-05-29
| |_|_|_|_|/ / / |/| | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 22:24:50 +0000