Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | | * | | | | Remove unused function Evd.whd_sort_variable | Gaëtan Gilbert | 2018-07-03 | |
| | | * | | | | Remove unused output of Universes.normalize_univ_variables | Gaëtan Gilbert | 2018-07-03 | |
| | | * | | | | Remove unused env argument to fresh_sort_in_family | Gaëtan Gilbert | 2018-07-03 | |
| | | * | | | | Coq_omega: remove unused Goal.enters | Gaëtan Gilbert | 2018-07-03 | |
| | | * | | | | Remove unused function Coq_omega.timing. | Gaëtan Gilbert | 2018-07-03 | |
| | | * | | | | Taccoerce: remove various unused arguments. | Gaëtan Gilbert | 2018-07-03 | |
| | | * | | | | Remove unused arguments to Ide_slave.concl_next_tac. | Gaëtan Gilbert | 2018-07-03 | |
| | | * | | | | Pptactic: remove unused arguments | Gaëtan Gilbert | 2018-07-03 | |
| | | * | | | | checker Indtypes: remove unused arguments | Gaëtan Gilbert | 2018-07-03 | |
| | | * | | | | Term_typing: remove unused argument to internal function. | Gaëtan Gilbert | 2018-07-03 | |
| | | * | | | | Cooking.cook_constant: remove unused env argument. | Gaëtan Gilbert | 2018-07-03 | |
| | | * | | | | Indtypes: remove unused is_unit. | Gaëtan Gilbert | 2018-07-03 | |
* | | | | | | | Merge PR #7607: Simplify reification of predicate in bytecode and native comp... | Pierre-Marie Pédrot | 2018-07-03 | |
|\ \ \ \ \ \ \ | ||||
| | | | * | | | | checker Modops strengthening: remove unused argument resolver | Gaëtan Gilbert | 2018-07-03 | |
| | | | * | | | | Subtyping.check_constant: remove unused module path argument. | Gaëtan Gilbert | 2018-07-03 | |
| | | | * | | | | Inductive.extract_stack,filter_stack_domain: remove unused arguments | Gaëtan Gilbert | 2018-07-03 | |
| | | | * | | | | Nativecode compile_mind, compile_mind_field: remove unused arguments | Gaëtan Gilbert | 2018-07-03 | |
| | | | * | | | | Nativecode.pp_mllam internal pp_letrec: remove unused argument. | Gaëtan Gilbert | 2018-07-03 | |
| | | | * | | | | Util.Empty: implement using polymorphic record. | Gaëtan Gilbert | 2018-07-03 | |
| | | | * | | | | coqdoc Index.find_string: remove unused argument. | Gaëtan Gilbert | 2018-07-03 | |
| | | | * | | | | Coq_makefile.generate_conf_coq_config: remove unused argument. | Gaëtan Gilbert | 2018-07-03 | |
| | | | * | | | | Libobject.apply_dyn_fun: remove unused deflt argument | Gaëtan Gilbert | 2018-07-03 | |
| | | | * | | | | CWarnings.normalize_flags: removed unused ~silent argument. | Gaëtan Gilbert | 2018-07-03 | |
| | | | * | | | | Modops.add_retroknowledge: remove unused argument. | Gaëtan Gilbert | 2018-07-03 | |
| |_|_|/ / / / |/| | | | | | | ||||
* | | | | | | | Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commands | Pierre-Marie Pédrot | 2018-07-03 | |
|\ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ | Merge PR #7942: Extend readme with 'beginners guide' | Théo Zimmermann | 2018-07-03 | |
|\ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ | Merge PR #7974: Fix default.nix following a package renaming. | Vincent Laporte | 2018-07-03 | |
|\ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ | Merge PR #7977: allow `make check` to succeed when -prefix is given to ./conf... | Emilio Jesus Gallego Arias | 2018-07-03 | |
|\ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | * | | | | | [ci] [docker] Make sure we don't install optional packages with apt. | Emilio Jesus Gallego Arias | 2018-07-02 | |
* | | | | | | | | | | | Merge PR #7703: Add an option to force parameters to be uniform | Matthieu Sozeau | 2018-07-02 | |
|\ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | * | | | | Rename the "chan" argument into "fmt" in coqpp_main. | Pierre-Marie Pédrot | 2018-07-02 | |
| | | | | | | | * | | | | Remove the hardcoded compatibility wit_hyp -> wit_var from the parser. | Pierre-Marie Pédrot | 2018-07-02 | |
| | | | | | | | * | | | | Slight simplification of the Tacentries API to register ML tactics. | Pierre-Marie Pédrot | 2018-07-02 | |
| | | | | | | | * | | | | Documenting the syntax changes. | Pierre-Marie Pédrot | 2018-07-02 | |
| | | | | | | | * | | | | Moving various ml4 files to mlg. | Pierre-Marie Pédrot | 2018-07-02 | |
| | | | | | | | * | | | | Implementing TACTIC EXTEND in coqpp. | Pierre-Marie Pédrot | 2018-07-02 | |
| | | | | | | |/ / / / | ||||
| | | | | * | | | | | | Add Equations overlay | Matthieu Sozeau | 2018-07-02 | |
* | | | | | | | | | | | Merge PR #7969: doc: typesetting and hyperlinks in Syntax Extensions | Théo Zimmermann | 2018-07-02 | |
|\ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7965: doc: Fix typesetting in Gallina extensions | Théo Zimmermann | 2018-07-02 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | ||||
| | | | | | * | | | | | | Clean up documentation around beginner's guide. | Siddharth Bhat | 2018-07-02 | |
| |_|_|_|_|/ / / / / / |/| | | | | | | | | | | ||||
| | | | * | | | | | | | [envars] honor env variable COQLIB | Enrico Tassi | 2018-07-02 | |
| | | | | | * | | | | | hints: add Hint Variables/Constants Opaque/Transparent commands | Matthieu Sozeau | 2018-07-02 | |
| |_|_|_|_|/ / / / / |/| | | | | | | | | | ||||
* | | | | | | | | | | Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension points... | Emilio Jesus Gallego Arias | 2018-07-02 | |
|\ \ \ \ \ \ \ \ \ \ | |_|_|_|/ / / / / / |/| | | | | | | | | | ||||
* | | | | | | | | | | Merge PR #7961: [api] Fix wrong deprecation warning (#7915) | Enrico Tassi | 2018-07-02 | |
|\ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | * | | | | | Adding back ocp-index to default.nix. | Théo Zimmermann | 2018-07-02 | |
| | | | | | * | | | | | Fix default.nix following a package renaming. | Théo Zimmermann | 2018-07-02 | |
| |_|_|_|_|/ / / / / |/| | | | | | | | | | ||||
| | | | | * | | | | | Document option Uniform Inductive Parameters | Jasper Hugunin | 2018-07-01 | |
| | | | | * | | | | | Add test for Uniform Inductive Parameters | Jasper Hugunin | 2018-07-01 | |
| | | | | * | | | | | Add flag Uniform Inductive Parameters | Jasper Hugunin | 2018-07-01 | |
| | | | | * | | | | | Implement uniform parameters in ComInductive | Jasper Hugunin | 2018-07-01 | |
| |_|_|_|/ / / / / |/| | | | | | | | |