aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-07-04Adapting to move of register_constr_interp0 from Pretyping to GlobEnv.Hugo Herbelin
2018-07-04Print something after the build completed if it wasn't a runner failure.Théo Zimmermann
This can then be leveraged by @coqbot to know which builds to restart.
2018-07-04[ci] Avoid annoying detached head warning.Emilio Jesus Gallego Arias
2018-07-04Make bin/ in makefile, not configure.Gaëtan Gilbert
2018-07-03Add a shell.nix that is not pinned to satisfy some developers' preference.Théo Zimmermann
2018-07-03Refactor default.nix to use optionals.Théo Zimmermann
2018-07-03Fix timing tools on NixOS.Théo Zimmermann
2018-07-03[test suite] Test case for attributesVincent Laporte
2018-07-03Document attributes.Vincent Laporte
2018-07-03fix syntax of .mlgVincent Laporte
2018-07-03Describe attributes in the documentation.Vincent Laporte
2018-07-03[vernac] use a record for the contents of the “deprecated” attributeVincent Laporte
2018-07-03[vernac] use plain strings as attribute namesVincent Laporte
The concrete syntax is still restricted to identifiers.
2018-07-03[vernac] indentationVincent Laporte
2018-07-03[vernac] Generic syntax for flags/attributesVincent Laporte
2018-07-03[vernac] Generic parsing rules for attributesVincent Laporte
2018-07-03[vernac] Add a “deprecated” attributeVincent Laporte
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-05 22:44:49 +0000