aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
| | | * | | | Pputils: fix typoGravatar Gaëtan Gilbert2018-07-03
| | | * | | | Evarutil.(e_)new_Type: remove unused env argumentGravatar Gaëtan Gilbert2018-07-03
| | | * | | | Remove unused function Evd.whd_sort_variableGravatar Gaëtan Gilbert2018-07-03
| | | * | | | Remove unused output of Universes.normalize_univ_variablesGravatar Gaëtan Gilbert2018-07-03
| | | * | | | Remove unused env argument to fresh_sort_in_familyGravatar Gaëtan Gilbert2018-07-03
| | | * | | | Coq_omega: remove unused Goal.entersGravatar Gaëtan Gilbert2018-07-03
| | | * | | | Remove unused function Coq_omega.timing.Gravatar Gaëtan Gilbert2018-07-03
| | | * | | | Taccoerce: remove various unused arguments.Gravatar Gaëtan Gilbert2018-07-03
| | | * | | | Remove unused arguments to Ide_slave.concl_next_tac.Gravatar Gaëtan Gilbert2018-07-03
| | | * | | | Pptactic: remove unused argumentsGravatar Gaëtan Gilbert2018-07-03
| | | * | | | checker Indtypes: remove unused argumentsGravatar Gaëtan Gilbert2018-07-03
| | | * | | | Term_typing: remove unused argument to internal function.Gravatar Gaëtan Gilbert2018-07-03
| | | * | | | Cooking.cook_constant: remove unused env argument.Gravatar Gaëtan Gilbert2018-07-03
| | | * | | | Indtypes: remove unused is_unit.Gravatar Gaëtan Gilbert2018-07-03
* | | | | | | Merge PR #7607: Simplify reification of predicate in bytecode and native comp...Gravatar Pierre-Marie Pédrot2018-07-03
|\ \ \ \ \ \ \
| | | | * | | | checker Modops strengthening: remove unused argument resolverGravatar Gaëtan Gilbert2018-07-03
| | | | * | | | Subtyping.check_constant: remove unused module path argument.Gravatar Gaëtan Gilbert2018-07-03
| | | | * | | | Inductive.extract_stack,filter_stack_domain: remove unused argumentsGravatar Gaëtan Gilbert2018-07-03
| | | | * | | | Nativecode compile_mind, compile_mind_field: remove unused argumentsGravatar Gaëtan Gilbert2018-07-03
| | | | * | | | Nativecode.pp_mllam internal pp_letrec: remove unused argument.Gravatar Gaëtan Gilbert2018-07-03
| | | | * | | | Util.Empty: implement using polymorphic record.Gravatar Gaëtan Gilbert2018-07-03
| | | | * | | | coqdoc Index.find_string: remove unused argument.Gravatar Gaëtan Gilbert2018-07-03
| | | | * | | | Coq_makefile.generate_conf_coq_config: remove unused argument.Gravatar Gaëtan Gilbert2018-07-03
| | | | * | | | Libobject.apply_dyn_fun: remove unused deflt argumentGravatar Gaëtan Gilbert2018-07-03
| | | | * | | | CWarnings.normalize_flags: removed unused ~silent argument.Gravatar Gaëtan Gilbert2018-07-03
| | | | * | | | Modops.add_retroknowledge: remove unused argument.Gravatar Gaëtan Gilbert2018-07-03
| |_|_|/ / / / |/| | | | | |
* | | | | | | Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commandsGravatar Pierre-Marie Pédrot2018-07-03
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #7942: Extend readme with 'beginners guide'Gravatar Théo Zimmermann2018-07-03
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #7974: Fix default.nix following a package renaming.Gravatar Vincent Laporte2018-07-03
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #7977: allow `make check` to succeed when -prefix is given to ./conf...Gravatar Emilio Jesus Gallego Arias2018-07-03
|\ \ \ \ \ \ \ \ \ \
| | | | | | * | | | | [ci] [docker] Make sure we don't install optional packages with apt.Gravatar Emilio Jesus Gallego Arias2018-07-02
* | | | | | | | | | | Merge PR #7703: Add an option to force parameters to be uniformGravatar Matthieu Sozeau2018-07-02
|\ \ \ \ \ \ \ \ \ \ \
| | | | | | | | * | | | Rename the "chan" argument into "fmt" in coqpp_main.Gravatar Pierre-Marie Pédrot2018-07-02
| | | | | | | | * | | | Remove the hardcoded compatibility wit_hyp -> wit_var from the parser.Gravatar Pierre-Marie Pédrot2018-07-02
| | | | | | | | * | | | Slight simplification of the Tacentries API to register ML tactics.Gravatar Pierre-Marie Pédrot2018-07-02
| | | | | | | | * | | | Documenting the syntax changes.Gravatar Pierre-Marie Pédrot2018-07-02
| | | | | | | | * | | | Moving various ml4 files to mlg.Gravatar Pierre-Marie Pédrot2018-07-02
| | | | | | | | * | | | Implementing TACTIC EXTEND in coqpp.Gravatar Pierre-Marie Pédrot2018-07-02
| | | | | | | |/ / / /
| | | | | * | | | | | Add Equations overlayGravatar Matthieu Sozeau2018-07-02
* | | | | | | | | | | Merge PR #7969: doc: typesetting and hyperlinks in Syntax ExtensionsGravatar Théo Zimmermann2018-07-02
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #7965: doc: Fix typesetting in Gallina extensionsGravatar Théo Zimmermann2018-07-02
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | |
| | | | | | * | | | | | Clean up documentation around beginner's guide.Gravatar Siddharth Bhat2018-07-02
| |_|_|_|_|/ / / / / / |/| | | | | | | | | |
| | | | * | | | | | | [envars] honor env variable COQLIBGravatar Enrico Tassi2018-07-02
| | | | | | * | | | | hints: add Hint Variables/Constants Opaque/Transparent commandsGravatar Matthieu Sozeau2018-07-02
| |_|_|_|_|/ / / / / |/| | | | | | | | |
* | | | | | | | | | Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension points...Gravatar Emilio Jesus Gallego Arias2018-07-02
|\ \ \ \ \ \ \ \ \ \ | |_|_|_|/ / / / / / |/| | | | | | | | |
* | | | | | | | | | Merge PR #7961: [api] Fix wrong deprecation warning (#7915)Gravatar Enrico Tassi2018-07-02
|\ \ \ \ \ \ \ \ \ \
| | | | | | * | | | | Adding back ocp-index to default.nix.Gravatar Théo Zimmermann2018-07-02
| | | | | | * | | | | Fix default.nix following a package renaming.Gravatar Théo Zimmermann2018-07-02
| |_|_|_|_|/ / / / / |/| | | | | | | | |
| | | | | * | | | | Document option Uniform Inductive ParametersGravatar Jasper Hugunin2018-07-01
| | | | | * | | | | Add test for Uniform Inductive ParametersGravatar Jasper Hugunin2018-07-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 01:05:56 +0000