aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-11-02Remove is_universe_polymorphism in funindGaëtan Gilbert
2018-11-02Remove is_universe_polymorphic in indschemesGaëtan Gilbert
2018-11-02Remove evdref style in build_combined_schemeGaëtan Gilbert
2018-11-02Generalize attributes further to get a monad (mostly for [map])Gaëtan Gilbert
2018-11-02Make attributes more general to make defining #[universes(...)] easyGaëtan Gilbert
2018-11-02Command driven attributes.Gaëtan Gilbert
2018-11-02Remove pointless optional arguments to mk_attsGaëtan Gilbert
2018-11-02{Vernacentries -> Attributes}.attributes_of_flagsGaëtan Gilbert
2018-11-02Remove location field from attributesGaëtan Gilbert
2018-11-02Move attributes out of vernacinterp to new attributes moduleGaëtan Gilbert
2018-11-02gitignore test-suite/misc/poly-capture-global-univs/src/evil.mlGaëtan Gilbert
2018-11-02[dev doc] Update proof engine docs, fixes #6640Emilio Jesus Gallego Arias
2018-11-02Fixing one instance of bug #8224 (grounding term w/o knowing if it has evars).Hugo Herbelin
2018-11-01Fix alphabetical orderVincent Semeria
2018-11-01develop constructive epsilonVincent Semeria
2018-11-01Fix creditsVincent Semeria
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
2018-10-31Partial fix of #8706 (tactic-in-term sensitive to seemingly unrelated scopes).Hugo Herbelin
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
2018-10-31Merge PR #8752: Enable fragile pattern warning in cclosureMaxime Dénès
2018-10-31Merge PR #8759: Fix #8755: Uncaught exception Ltac_plugin.Taccoerce.CannotCoe...Hugo Herbelin
2018-10-31Fix #8881: validate fails to use inductive equivalence in case_infoGaëtan Gilbert
2018-10-31Merge PR #8841: Share the construction of the evar instance in Clenv.make_eva...Matthieu Sozeau
2018-10-31Fix #8876: expected number of arguments for cumulative constructorsGaëtan Gilbert
2018-10-31Merge PR #8867: Notations: fixing a bug when printing abbreviations in custom...Emilio Jesus Gallego Arias
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
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
2018-10-31[nametab] Move global_dir_reference to NametabEmilio Jesus Gallego Arias
2018-10-31Merge PR #8688: Generalizing the various evar_map printers in Termops over an...Pierre-Marie Pédrot
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
2018-10-31Notations: fixing a bug with abbreviations in custom entries.Hugo Herbelin
2018-10-31Merge PR #8851: Credits for 8.9Guillaume Melquiond
2018-10-31Merge PR #8849: Fix for bug #8848.Pierre-Marie Pédrot
2018-10-30Remove Environ.set_universes / Typing.enrich_envGaëtan Gilbert
2018-10-30Check univ instances in Typing.Gaëtan Gilbert
2018-10-30Fix evar leak in induction tactic.Gaëtan Gilbert
2018-10-30Simplify universe handling in environ constant_type functionsGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 05:57:22 +0000