aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
| | | * | | | Pputils: fix typoGravatar Gaëtan Gilbert2018-07-03
| | | | | | |
| | | * | | | Evarutil.(e_)new_Type: remove unused env argumentGravatar Gaëtan Gilbert2018-07-03
| | | | | | |
| | | * | | | Remove unused function Evd.whd_sort_variableGravatar Gaëtan Gilbert2018-07-03
| | | | | | |
| | | * | | | Remove unused output of Universes.normalize_univ_variablesGravatar Gaëtan Gilbert2018-07-03
| | | | | | |
| | | * | | | Remove unused env argument to fresh_sort_in_familyGravatar Gaëtan Gilbert2018-07-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | (Universes and Evd)
| | | * | | | Coq_omega: remove unused Goal.entersGravatar Gaëtan Gilbert2018-07-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Unused since fd7f056b155b2ebaafa3251a3c136117ebefc3e3.
| | | * | | | Remove unused function Coq_omega.timing.Gravatar Gaëtan Gilbert2018-07-03
| | | | | | |
| | | * | | | Taccoerce: remove various unused arguments.Gravatar Gaëtan Gilbert2018-07-03
| | | | | | |
| | | * | | | Remove unused arguments to Ide_slave.concl_next_tac.Gravatar Gaëtan Gilbert2018-07-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Unused since 2285dae8af54043090ce5f8a59aa4162679714c6
| | | * | | | Pptactic: remove unused argumentsGravatar Gaëtan Gilbert2018-07-03
| | | | | | |
| | | * | | | checker Indtypes: remove unused argumentsGravatar Gaëtan Gilbert2018-07-03
| | | | | | |
| | | * | | | Term_typing: remove unused argument to internal function.Gravatar Gaëtan Gilbert2018-07-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The function is defined with a typo but called with the same env that is mistakenly not shadowed. An alternative to this commit would be to fix the typo.
| | | * | | | Cooking.cook_constant: remove unused env argument.Gravatar Gaëtan Gilbert2018-07-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Unused since d95306323 (remove template polymorphic definitions).
| | | * | | | Indtypes: remove unused is_unit.Gravatar Gaëtan Gilbert2018-07-03
| | | | | | |
* | | | | | | Merge PR #7607: Simplify reification of predicate in bytecode and native ↵Gravatar Pierre-Marie Pédrot2018-07-03
|\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | compilers
| | | | * | | | checker Modops strengthening: remove unused argument resolverGravatar Gaëtan Gilbert2018-07-03
| | | | | | | |
| | | | * | | | Subtyping.check_constant: remove unused module path argument.Gravatar Gaëtan Gilbert2018-07-03
| | | | | | | |
| | | | * | | | Inductive.extract_stack,filter_stack_domain: remove unused argumentsGravatar Gaëtan Gilbert2018-07-03
| | | | | | | |
| | | | * | | | Nativecode compile_mind, compile_mind_field: remove unused argumentsGravatar Gaëtan Gilbert2018-07-03
| | | | | | | |
| | | | * | | | Nativecode.pp_mllam internal pp_letrec: remove unused argument.Gravatar Gaëtan Gilbert2018-07-03
| | | | | | | |
| | | | * | | | Util.Empty: implement using polymorphic record.Gravatar Gaëtan Gilbert2018-07-03
| | | | | | | |
| | | | * | | | coqdoc Index.find_string: remove unused argument.Gravatar Gaëtan Gilbert2018-07-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Unused since 6832c60f741e6bfb2a850d567fd6a1dff7059393.
| | | | * | | | Coq_makefile.generate_conf_coq_config: remove unused argument.Gravatar Gaëtan Gilbert2018-07-03
| | | | | | | |
| | | | * | | | Libobject.apply_dyn_fun: remove unused deflt argumentGravatar Gaëtan Gilbert2018-07-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Unused since 8e07227c5853de78eaed4577eefe908fb84507c0.
| | | | * | | | CWarnings.normalize_flags: removed unused ~silent argument.Gravatar Gaëtan Gilbert2018-07-03
| | | | | | | |
| | | | * | | | Modops.add_retroknowledge: remove unused argument.Gravatar Gaëtan Gilbert2018-07-03
| |_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Unused since fe1979bf47951352ce32a6709cb5138fd26f311d. I'm not sure if it was actually used back then since I didn't look at the function it was passed to.
* | | | | | | Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commandsGravatar Pierre-Marie Pédrot2018-07-03
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #7942: Extend readme with 'beginners guide'Gravatar Théo Zimmermann2018-07-03
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #7974: Fix default.nix following a package renaming.Gravatar Vincent Laporte2018-07-03
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #7977: allow `make check` to succeed when -prefix is given to ↵Gravatar Emilio Jesus Gallego Arias2018-07-03
|\ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ./configure and make install not run yet
| | | | | | * | | | | [ci] [docker] Make sure we don't install optional packages with apt.Gravatar Emilio Jesus Gallego Arias2018-07-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This should help towards ensuring that the system only has the packages we specify in the Dockerfile. We were missing: - `git`: used in the CI system itself! - `rsync`: used in the test-suite - `python3-setuptools`, `python3-wheel`: necessary to use pip3 properly to install the missing python package. - `autoconf`, `automake`: a few CI contribs depend on them.
* | | | | | | | | | | Merge PR #7703: Add an option to force parameters to be uniformGravatar Matthieu Sozeau2018-07-02
|\ \ \ \ \ \ \ \ \ \ \
| | | | | | | | * | | | Rename the "chan" argument into "fmt" in coqpp_main.Gravatar Pierre-Marie Pédrot2018-07-02
| | | | | | | | | | | |
| | | | | | | | * | | | Remove the hardcoded compatibility wit_hyp -> wit_var from the parser.Gravatar Pierre-Marie Pédrot2018-07-02
| | | | | | | | | | | |
| | | | | | | | * | | | Slight simplification of the Tacentries API to register ML tactics.Gravatar Pierre-Marie Pédrot2018-07-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It was forcing the macro to generate code that was useless.
| | | | | | | | * | | | Documenting the syntax changes.Gravatar Pierre-Marie Pédrot2018-07-02
| | | | | | | | | | | |
| | | | | | | | * | | | Moving various ml4 files to mlg.Gravatar Pierre-Marie Pédrot2018-07-02
| | | | | | | | | | | |
| | | | | | | | * | | | Implementing TACTIC EXTEND in coqpp.Gravatar Pierre-Marie Pédrot2018-07-02
| | | | | | | |/ / / /
| | | | | * | | | | | Add Equations overlayGravatar Matthieu Sozeau2018-07-02
| | | | | | | | | | |
* | | | | | | | | | | Merge PR #7969: doc: typesetting and hyperlinks in Syntax ExtensionsGravatar Théo Zimmermann2018-07-02
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #7965: doc: Fix typesetting in Gallina extensionsGravatar Théo Zimmermann2018-07-02
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | |
| | | | | | * | | | | | Clean up documentation around beginner's guide.Gravatar Siddharth Bhat2018-07-02
| |_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - move `README` to `README.md` to take advantage of markdown features - remove `setup.txt`, port the editor specific information to the wiki. Merge development information into `dev/doc/README.md`. Wiki merge link: https://github.com/coq/coq/wiki/DevelSetup. - Add new links to files into `dev/README.md`. - Remove stale `translate.txt`.
| | | | * | | | | | | [envars] honor env variable COQLIBGravatar Enrico Tassi2018-07-02
| | | | | | | | | | |
| | | | | | * | | | | hints: add Hint Variables/Constants Opaque/Transparent commandsGravatar Matthieu Sozeau2018-07-02
| |_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This gives user control on the transparent state of a hint db. Can override defaults more easily (report by J. H. Jourdan). For "core", declare that variables can be unfolded, but no constants (ensures compatibility with previous auto which allowed conv on closed terms) Document Hint Variables
* | | | | | | | | | Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension ↵Gravatar Emilio Jesus Gallego Arias2018-07-02
|\ \ \ \ \ \ \ \ \ \ | |_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | | | points of Camlp5
* | | | | | | | | | Merge PR #7961: [api] Fix wrong deprecation warning (#7915)Gravatar Enrico Tassi2018-07-02
|\ \ \ \ \ \ \ \ \ \
| | | | | | * | | | | Adding back ocp-index to default.nix.Gravatar Théo Zimmermann2018-07-02
| | | | | | | | | | |
| | | | | | * | | | | Fix default.nix following a package renaming.Gravatar Théo Zimmermann2018-07-02
| |_|_|_|_|/ / / / / |/| | | | | | | | |
| | | | | * | | | | Document option Uniform Inductive ParametersGravatar Jasper Hugunin2018-07-01
| | | | | | | | | |
| | | | | * | | | | Add test for Uniform Inductive ParametersGravatar Jasper Hugunin2018-07-01
| | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 20:48:02 +0000