aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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-02Merge PR #7703: Add an option to force parameters to be uniformMatthieu Sozeau
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
2018-07-01Merge PR #7760: Fixes #7712 (an anomaly in reporting bad recursive notation ↵Emilio Jesus Gallego Arias
format).
2018-07-01Merge PR #7759: Workaround to fix #7731 (printing not splitting line at ↵Emilio Jesus Gallego Arias
break hint).
2018-06-30doc: typesetting and hyperlinks in Syntax ExtensionsLysxia
2018-06-30Merge PR #7960: [build] Remove target binary before copy.Enrico Tassi
2018-06-30Merge PR #7949: Split the Ssrmatching module between code and grammar rules.Enrico Tassi
2018-06-30Split the Ssrmatching module between code and grammar rules.Pierre-Marie Pédrot
Fixes #7857.
2018-06-29Adding an overlay for the PR.Pierre-Marie Pédrot
2018-06-29Documenting the transition strategy of GEXTEND.Pierre-Marie Pédrot
2018-06-29Port g_tactic to the homebrew GEXTEND parser.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 07:59:43 +0000