aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-11-01Fix header and doc indexVincent Semeria
2018-11-01proof that R is uncountableVincent Semeria
2018-11-01Merge PR #8845: Fix typos in the document about CICThéo Zimmermann
2018-10-31Fixes rest of #3468 (tactic-in-term was not respecting scopes).Hugo Herbelin
We do it by passing interning env to ltac interning. Collecting scopes was already done by side-effect internally to Constrintern. We expose the side-effect to ltac.
2018-10-31Partial fix of #8706 (tactic-in-term sensitive to seemingly unrelated scopes).Hugo Herbelin
We compute the binding to tactic-in-term once for all in the right scopes before interpreting the tactic. An alternative would have been to surround the constr_expr by CDelimiters to simulate its interpretation in the expected scopes (though this would not have worked for temporary scopes).
2018-10-31Clarify meaning of boolean in IPatDispatchMaxime Dénès
2018-10-31[ssr] better doc for the IPatDispatch ASTEnrico Tassi
2018-10-31test-suite entry for issue #8544Cyril Cohen
2018-10-31[ssr] use tclDISPATCH for IPatDispatch (fix #8544)Enrico Tassi
2018-10-31Use standard combinator for Global.set_strategyMaxime Dénès
2018-10-31Introduce Safe_typing.set_share_reductionMaxime Dénès
2018-10-31Seeing Global purely as a wrapper on top of kernel functions.Hugo Herbelin
2018-10-31Renaming is_template_polymorphic -> is_template_polymorphic_ind.Hugo Herbelin
This emphasizes that it works only on inductive types. Also, the name is_template_polymorphic will be reused for a more general version.
2018-10-31Merge PR #8752: Enable fragile pattern warning in cclosureMaxime Dénès
2018-10-31Merge PR #8759: Fix #8755: Uncaught exception ↵Hugo Herbelin
Ltac_plugin.Taccoerce.CannotCoerceTo.
2018-10-31Fix #8881: validate fails to use inductive equivalence in case_infoGaëtan Gilbert
See also 55dbe8e2fa7ed2053ecd54140f6bcbdf31981e0b
2018-10-31Merge PR #8841: Share the construction of the evar instance in ↵Matthieu Sozeau
Clenv.make_evar_clause.
2018-10-31Fix #8876: expected number of arguments for cumulative constructorsGaëtan Gilbert
ee573583701c8e53e8b82978998a9df93170cd79 ported to the checker.
2018-10-31Merge PR #8867: Notations: fixing a bug when printing abbreviations in ↵Emilio Jesus Gallego Arias
custom entries.
2018-10-31Fix #8873: coqchk on inductive with letin parameterGaëtan Gilbert
2018-10-31No need to require List in test-suite/success/Inductive.vGaëtan Gilbert
Requires are slow in the debugger so removing this makes it nicer to debug.
2018-10-31Merge PR #8864: Avoid passing empty environmentsPierre-Marie Pédrot
2018-10-31[nametab] Move `object_prefix` to `Nametab`.Emilio Jesus Gallego Arias
We move `object_prefix` to `Nametab`. This highlights the coupling of `Lib` and `Nametab` wrt naming. This also thins `Libname`, which IMHO is a good thing as we are talking about "local, internal" naming here.
2018-10-31[nametab] Move global_dir_reference to NametabEmilio Jesus Gallego Arias
This type is "private" to the Nametab, which manages it. It thus makes sense IMHO to live there.
2018-10-31Merge PR #8688: Generalizing the various evar_map printers in Termops over ↵Pierre-Marie Pédrot
an environment
2018-10-31Merge PR #8825: [libobject] Move object_name next to object definition.Pierre-Marie Pédrot
2018-10-31[library] Better sizing for libobject hashtbl.Emilio Jesus Gallego Arias
17 is a very small number as files in the stdlib will routinely pass size 190. As this is done only on startup, it seems wise to provide a bit more space.
2018-10-31Notations: fixing a bug with abbreviations in custom entries.Hugo Herbelin
Coercions were missing.
2018-10-31Merge PR #8851: Credits for 8.9Guillaume Melquiond
2018-10-31Revert "Merge pull request #13 from ↵Yves Bertot
herbelin/master+adapt-coq8718-declaration-hooks" This reverts commit 9e8d0b077d8021e468ec0bc117438695c0b243bf, reversing changes made to 56c3ae6296994cc288d4931110118617bb5bb978.
2018-10-31Merge PR #8849: Fix for bug #8848.Pierre-Marie Pédrot
2018-10-30Remove Environ.set_universes / Typing.enrich_envGaëtan Gilbert
Made possible by the previous commit passing ~evars to check_hyps_inclusion.
2018-10-30Check univ instances in Typing.Gaëtan Gilbert
2018-10-30Fix evar leak in induction tactic.Gaëtan Gilbert
Detected when making Typing check universe instances.
2018-10-30Simplify universe handling in environ constant_type functionsGaëtan Gilbert
2018-10-30Merge PR #8750: [ci] [doc] Notes about branch names.Gaëtan Gilbert
2018-10-30Credits for 8.9Matthieu Sozeau
Adressed comments by Guillaume and Jason Updated according to Zimmi48's input. Better link to custom entries Fix typesetting
2018-10-30Merge pull request #13 from herbelin/master+adapt-coq8718-declaration-hooksYves Bertot
Adapting to Coq PR #8718: declare_definition now takes a UState.t + using new predefined no_hook
2018-10-30Adapting to Coq PR #8718: declare_definition now takes a UState.t.Hugo Herbelin
Also use new predefined Lemmas.no_kook.
2018-10-30Overlays (#8844 split-tactics)Gaëtan Gilbert
2018-10-30Adding overlay for coq-elpiHugo Herbelin
2018-10-30Generalizing the various evar_map printers in Termops over an environment.Hugo Herbelin
This is a step towards limiting calls to the global environment. Incidentally unify naming evd -> sigma in Termops.
2018-10-30Remove fully_empty_glob_sign which uses a dummy environmentMaxime Dénès
2018-10-30Avoid passing dummy env to error printerMaxime Dénès
2018-10-30Reduction functions based on CClosure should take an envMaxime Dénès
This is because the env contains typing flags (such as sharing strategy).
2018-10-30Remove one use of empty_env in ssrMaxime Dénès
2018-10-30Avoid redefining reduction functions in fun_indMaxime Dénès
We also stop passing dummy env and evar maps.
2018-10-30Distinguish globalization and pretyping error on unbound variableMaxime Dénès
We can then avoid passing an empty env.
2018-10-30Adapt to coq/coq#8844 (move abstract out of tactics.ml)Gaëtan Gilbert
2018-10-30Move abstract out of tactics.mlGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-04 20:17:29 +0000