aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2018-07-02[ci] [docker] Make sure we don't install optional packages with apt.Emilio Jesus Gallego Arias
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
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
2018-07-02[envars] honor env variable COQLIBEnrico Tassi
2018-07-02hints: add Hint Variables/Constants Opaque/Transparent commandsMatthieu Sozeau
2018-07-02Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension points...Emilio Jesus Gallego Arias
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
2018-07-01[api] Fix wrong deprecation warning (#7915)Emilio Jesus Gallego Arias
2018-07-01Merge PR #7964: Document that GITURL variables shouldn't have a trailing .git...Emilio Jesus Gallego Arias
2018-07-01Merge PR #7410: Splitting primitive numeral parser/printer for positive, N, Z...Emilio Jesus Gallego Arias