Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | | * | | | | Library: use ocaml typing to show that we find at most 2 files | 2018-07-03 | ||
| | | * | | | | Library.register_loaded_library: remove unused variable | 2018-07-03 | ||
| | | * | | | | Glob_ops.rename_glob_vars: fix typo | 2018-07-03 | ||
| | | * | | | | Glob_ops.fix_kind_eq: fix typo | 2018-07-03 | ||
| | | * | | | | Pputils: fix typo | 2018-07-03 | ||
| | | * | | | | Evarutil.(e_)new_Type: remove unused env argument | 2018-07-03 | ||
| | | * | | | | Remove unused function Evd.whd_sort_variable | 2018-07-03 | ||
| | | * | | | | Remove unused output of Universes.normalize_univ_variables | 2018-07-03 | ||
| | | * | | | | Remove unused env argument to fresh_sort_in_family | 2018-07-03 | ||
| | | * | | | | Coq_omega: remove unused Goal.enters | 2018-07-03 | ||
| | | * | | | | Remove unused function Coq_omega.timing. | 2018-07-03 | ||
| | | * | | | | Taccoerce: remove various unused arguments. | 2018-07-03 | ||
| | | * | | | | Remove unused arguments to Ide_slave.concl_next_tac. | 2018-07-03 | ||
| | | * | | | | Pptactic: remove unused arguments | 2018-07-03 | ||
| | | * | | | | checker Indtypes: remove unused arguments | 2018-07-03 | ||
| | | * | | | | Term_typing: remove unused argument to internal function. | 2018-07-03 | ||
| | | * | | | | Cooking.cook_constant: remove unused env argument. | 2018-07-03 | ||
| | | * | | | | Indtypes: remove unused is_unit. | 2018-07-03 | ||
* | | | | | | | Merge PR #7607: Simplify reification of predicate in bytecode and native comp... | 2018-07-03 | ||
|\ \ \ \ \ \ \ | ||||
| | | | * | | | | checker Modops strengthening: remove unused argument resolver | 2018-07-03 | ||
| | | | * | | | | Subtyping.check_constant: remove unused module path argument. | 2018-07-03 | ||
| | | | * | | | | Inductive.extract_stack,filter_stack_domain: remove unused arguments | 2018-07-03 | ||
| | | | * | | | | Nativecode compile_mind, compile_mind_field: remove unused arguments | 2018-07-03 | ||
| | | | * | | | | Nativecode.pp_mllam internal pp_letrec: remove unused argument. | 2018-07-03 | ||
| | | | * | | | | Util.Empty: implement using polymorphic record. | 2018-07-03 | ||
| | | | * | | | | coqdoc Index.find_string: remove unused argument. | 2018-07-03 | ||
| | | | * | | | | Coq_makefile.generate_conf_coq_config: remove unused argument. | 2018-07-03 | ||
| | | | * | | | | Libobject.apply_dyn_fun: remove unused deflt argument | 2018-07-03 | ||
| | | | * | | | | CWarnings.normalize_flags: removed unused ~silent argument. | 2018-07-03 | ||
| | | | * | | | | Modops.add_retroknowledge: remove unused argument. | 2018-07-03 | ||
| |_|_|/ / / / |/| | | | | | | ||||
* | | | | | | | Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commands | 2018-07-03 | ||
|\ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ | Merge PR #7942: Extend readme with 'beginners guide' | 2018-07-03 | ||
|\ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ | Merge PR #7974: Fix default.nix following a package renaming. | 2018-07-03 | ||
|\ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ | Merge PR #7977: allow `make check` to succeed when -prefix is given to ./conf... | 2018-07-03 | ||
|\ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | * | | | | | [ci] [docker] Make sure we don't install optional packages with apt. | 2018-07-02 | ||
* | | | | | | | | | | | Merge PR #7703: Add an option to force parameters to be uniform | 2018-07-02 | ||
|\ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | * | | | | Rename the "chan" argument into "fmt" in coqpp_main. | 2018-07-02 | ||
| | | | | | | | * | | | | Remove the hardcoded compatibility wit_hyp -> wit_var from the parser. | 2018-07-02 | ||
| | | | | | | | * | | | | Slight simplification of the Tacentries API to register ML tactics. | 2018-07-02 | ||
| | | | | | | | * | | | | Documenting the syntax changes. | 2018-07-02 | ||
| | | | | | | | * | | | | Moving various ml4 files to mlg. | 2018-07-02 | ||
| | | | | | | | * | | | | Implementing TACTIC EXTEND in coqpp. | 2018-07-02 | ||
| | | | | | | |/ / / / | ||||
| | | | | * | | | | | | Add Equations overlay | 2018-07-02 | ||
* | | | | | | | | | | | Merge PR #7969: doc: typesetting and hyperlinks in Syntax Extensions | 2018-07-02 | ||
|\ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7965: doc: Fix typesetting in Gallina extensions | 2018-07-02 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | ||||
| | | | | | * | | | | | | Clean up documentation around beginner's guide. | 2018-07-02 | ||
| |_|_|_|_|/ / / / / / |/| | | | | | | | | | | ||||
| | | | * | | | | | | | [envars] honor env variable COQLIB | 2018-07-02 | ||
| | | | | | * | | | | | hints: add Hint Variables/Constants Opaque/Transparent commands | 2018-07-02 | ||
| |_|_|_|_|/ / / / / |/| | | | | | | | | | ||||
* | | | | | | | | | | Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension points... | 2018-07-02 | ||
|\ \ \ \ \ \ \ \ \ \ | |_|_|_|/ / / / / / |/| | | | | | | | | | ||||
* | | | | | | | | | | Merge PR #7961: [api] Fix wrong deprecation warning (#7915) | 2018-07-02 | ||
|\ \ \ \ \ \ \ \ \ \ |