aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-07-03Coq_omega: remove unused Goal.entersGaëtan Gilbert
Unused since fd7f056b155b2ebaafa3251a3c136117ebefc3e3.
2018-07-03Remove unused function Coq_omega.timing.Gaëtan Gilbert
2018-07-03Taccoerce: remove various unused arguments.Gaëtan Gilbert
2018-07-03Remove unused arguments to Ide_slave.concl_next_tac.Gaëtan Gilbert
Unused since 2285dae8af54043090ce5f8a59aa4162679714c6
2018-07-03Pptactic: remove unused argumentsGaëtan Gilbert
2018-07-03checker Indtypes: remove unused argumentsGaëtan Gilbert
2018-07-03Term_typing: remove unused argument to internal function.Gaëtan Gilbert
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.
2018-07-03Cooking.cook_constant: remove unused env argument.Gaëtan Gilbert
Unused since d95306323 (remove template polymorphic definitions).
2018-07-03Indtypes: remove unused is_unit.Gaëtan Gilbert
2018-07-03Merge PR #7607: Simplify reification of predicate in bytecode and native ↵Pierre-Marie Pédrot
compilers
2018-07-03checker Modops strengthening: remove unused argument resolverGaëtan Gilbert
2018-07-03Subtyping.check_constant: remove unused module path argument.Gaëtan Gilbert
2018-07-03Inductive.extract_stack,filter_stack_domain: remove unused argumentsGaëtan Gilbert
2018-07-03Nativecode compile_mind, compile_mind_field: remove unused argumentsGaëtan Gilbert
2018-07-03Nativecode.pp_mllam internal pp_letrec: remove unused argument.Gaëtan Gilbert
2018-07-03Util.Empty: implement using polymorphic record.Gaëtan Gilbert
2018-07-03coqdoc Index.find_string: remove unused argument.Gaëtan Gilbert
Unused since 6832c60f741e6bfb2a850d567fd6a1dff7059393.
2018-07-03Coq_makefile.generate_conf_coq_config: remove unused argument.Gaëtan Gilbert
2018-07-03Libobject.apply_dyn_fun: remove unused deflt argumentGaëtan Gilbert
Unused since 8e07227c5853de78eaed4577eefe908fb84507c0.
2018-07-03CWarnings.normalize_flags: removed unused ~silent argument.Gaëtan Gilbert
2018-07-03Modops.add_retroknowledge: remove unused argument.Gaëtan Gilbert
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.
2018-07-03Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commandsPierre-Marie Pédrot
2018-07-03Merge PR #7942: Extend readme with 'beginners guide'Théo Zimmermann
2018-07-03Merge PR #7974: Fix default.nix following a package renaming.Vincent Laporte
2018-07-03Merge PR #7977: allow `make check` to succeed when -prefix is given to ↵Emilio Jesus Gallego Arias
./configure and make install not run yet
2018-07-02[ci] [docker] Make sure we don't install optional packages with apt.Emilio Jesus Gallego Arias
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.
2018-07-02Merge PR #7703: Add an option to force parameters to be uniformMatthieu Sozeau
2018-07-02Rename the "chan" argument into "fmt" in coqpp_main.Pierre-Marie Pédrot
2018-07-02Remove the hardcoded compatibility wit_hyp -> wit_var from the parser.Pierre-Marie Pédrot
2018-07-02Slight simplification of the Tacentries API to register ML tactics.Pierre-Marie Pédrot
It was forcing the macro to generate code that was useless.
2018-07-02Documenting the syntax changes.Pierre-Marie Pédrot
2018-07-02Moving various ml4 files to mlg.Pierre-Marie Pédrot
2018-07-02Implementing TACTIC EXTEND in coqpp.Pierre-Marie Pédrot
2018-07-02Add Equations overlayMatthieu Sozeau
2018-07-02Merge PR #7969: doc: typesetting and hyperlinks in Syntax ExtensionsThéo Zimmermann
2018-07-02Merge PR #7965: doc: Fix typesetting in Gallina extensionsThéo Zimmermann
2018-07-02Clean up documentation around beginner's guide.Siddharth Bhat
- 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`.
2018-07-02[envars] honor env variable COQLIBEnrico Tassi
2018-07-02hints: add Hint Variables/Constants Opaque/Transparent commandsMatthieu Sozeau
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
2018-07-02Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension ↵Emilio Jesus Gallego Arias
points of Camlp5
2018-07-02Merge PR #7961: [api] Fix wrong deprecation warning (#7915)Enrico Tassi
2018-07-02Adding back ocp-index to default.nix.Théo Zimmermann
2018-07-02Fix default.nix following a package renaming.Théo Zimmermann
2018-07-01Document option Uniform Inductive ParametersJasper Hugunin
2018-07-01Add test for Uniform Inductive ParametersJasper Hugunin
2018-07-01Add flag Uniform Inductive ParametersJasper Hugunin
2018-07-01Implement uniform parameters in ComInductiveJasper Hugunin
Don't allow notations attached to uniform inductives
2018-07-01[api] Fix wrong deprecation warning (#7915)Emilio Jesus Gallego Arias
Fixes: #7915. Due to a change in the original misctypes removal PR, the deprecation notice went out of sync.
2018-07-01Merge PR #7964: Document that GITURL variables shouldn't have a trailing ↵Emilio Jesus Gallego Arias
.git anymore.
2018-07-01Merge PR #7410: Splitting primitive numeral parser/printer for positive, N, ↵Emilio Jesus Gallego Arias
Z into three files
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 16:13:19 +0000