aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-07-05Merge PR #7746: Many small cleanups removing unused arguments and functionsPierre-Marie Pédrot
2018-07-05Merge PR #7979: TACTIC EXTEND in coqppEmilio Jesus Gallego Arias
2018-07-04Merge PR #7973: Add a test build on NixOS to GitLab CI.Gaëtan Gilbert
2018-07-04Merge PR #7989: [ci] Avoid annoying detached head warning.Gaëtan Gilbert
2018-07-04Merge PR #7993: doc: Fix markup in Calculus of Inductive ConstructionsThéo Zimmermann
2018-07-04doc: Fix markup in Calculus of Inductive ConstructionsFabian
2018-07-04Merge PR #7992: Print something after the build completed if it wasn't a runn...Gaëtan Gilbert
2018-07-04Print something after the build completed if it wasn't a runner failure.Théo Zimmermann
2018-07-04[ci] Avoid annoying detached head warning.Emilio Jesus Gallego Arias
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-03Add a test build of Nix package to GitLab CI.Théo Zimmermann
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 wi...Gaëtan Gilbert
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
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
2018-07-03Coq_omega: remove unused Goal.entersGaëtan Gilbert
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
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
2018-07-03Cooking.cook_constant: remove unused env argument.Gaëtan Gilbert
2018-07-03Indtypes: remove unused is_unit.Gaëtan Gilbert
2018-07-03Merge PR #7607: Simplify reification of predicate in bytecode and native comp...Pierre-Marie Pédrot
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
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
2018-07-03CWarnings.normalize_flags: removed unused ~silent argument.Gaëtan Gilbert
2018-07-03Modops.add_retroknowledge: remove unused argument.Gaëtan Gilbert
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 ./conf...Emilio Jesus Gallego Arias