aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-07-03Allow “Let”-defined coercionsVincent Laporte
2018-07-03[vernac] Concrete syntax for attributesVincent Laporte
2018-07-03[vernac] mk_atts: an atts record with default valuesVincent Laporte
2018-07-03[vernac] attribute_of_flagsVincent Laporte
Elaborate a [atts] record out of a list of flags.
2018-07-03Add a test build of Nix package to GitLab CI.Théo Zimmermann
We pin default.nix again to make the CI build predictable. As in Windows builds, we need to override the default before_script. As in other test-suite jobs, we export logs as artifacts on failure.
2018-07-03Adapt default.nix to allow nix-build to run the test-suite.Théo Zimmermann
2018-07-03Merge PR #7978: [ci] [docker] Make sure we don't install optional packages ↵Gaëtan Gilbert
with apt.
2018-07-03Add overlay for equations.Gaëtan Gilbert
2018-07-03Library: use ocaml typing to show that we find at most 2 filesGaëtan Gilbert
2018-07-03Library.register_loaded_library: remove unused variableGaëtan Gilbert
This one is a bit weird. Unused since 4d95eb4e878f375a69f1b48d8833801bf555fdd0 (kept semantics, the m is the same one outside and inside the call)
2018-07-03Glob_ops.rename_glob_vars: fix typoGaëtan Gilbert
2018-07-03Glob_ops.fix_kind_eq: fix typoGaëtan Gilbert
2018-07-03Pputils: fix typoGaëtan Gilbert
2018-07-03Evarutil.(e_)new_Type: remove unused env argumentGaëtan Gilbert
2018-07-03Remove unused function Evd.whd_sort_variableGaëtan Gilbert
2018-07-03Remove unused output of Universes.normalize_univ_variablesGaëtan Gilbert
2018-07-03Remove unused env argument to fresh_sort_in_familyGaëtan Gilbert
(Universes and Evd)
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-28 06:43:51 +0000