aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-11-02rewrite: attributes handle is_univ_poly, is_program_modeGaëtan Gilbert
2018-11-02Remove is_universe_polymorphism in funindGaëtan Gilbert
Funind doesn't support polymorphism.
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
Having [map] means we can structure attributes when combining them, eg get an attribute for [type universe_data = { poly : bool option; template : bool option }] from 2 [bool option] attributes. Using the previous representation we would have had to provide the inverse function [universe_data -> bool option * bool option] as well. An alternate way to get (++) is let (++) (x:'a t) (y:'b t) : ('a*'b) t = x >>= fun xv -> y >>= fun yv -> return (xv,yv) Not sure if that would be cleaner.
2018-11-02Make attributes more general to make defining #[universes(...)] easyGaëtan Gilbert
2018-11-02Command driven attributes.Gaëtan Gilbert
Commands need to request the attributes they use, with the API encouraging them to error on unsupported attributes.
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
It was never set, because it makes no sense.
2018-11-02Move attributes out of vernacinterp to new attributes moduleGaëtan Gilbert
2018-11-01Merge PR #8845: Fix typos in the document about CICThéo Zimmermann
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-31Merge PR #8841: Share the construction of the evar instance in ↵Matthieu Sozeau
Clenv.make_evar_clause.
2018-10-31Merge PR #8867: Notations: fixing a bug when printing abbreviations in ↵Emilio Jesus Gallego Arias
custom entries.
2018-10-31Merge PR #8864: Avoid passing empty environmentsPierre-Marie Pédrot
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-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-31Merge PR #8849: Fix for bug #8848.Pierre-Marie Pédrot
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-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-29Fix for bug #8848Matthieu Sozeau
2018-10-29Merge PR #8751: Rename checker/{main->coqchk}Pierre-Marie Pédrot
2018-10-29Fix typos in the document about CICwkwkes
2018-10-29Merge PR #8765: Give code ownership of merging doc to pushers team to notify ↵Maxime Dénès
members when it changes.
2018-10-29Merge PR #8667: [RFC] Vendoring of Camlp5Pierre-Marie Pédrot
2018-10-29Merge PR #8711: [ci] [appveyor] Enable cache for builds.Maxime Dénès
2018-10-29Merge PR #8737: Correctly report non-projection fields in recordsPierre-Marie Pédrot
2018-10-29Merge PR #8780: Cleanup comparing projections through their constants.Maxime Dénès
2018-10-29Rename checker/{main->coqchk}Gaëtan Gilbert
2018-10-29Share the construction of the evar instance in Clenv.make_evar_clause.Pierre-Marie Pédrot
Fixes most of #8822.
2018-10-29Merge PR #8763: Adapt coq_makefile to handle coqpp-based macro files.Enrico Tassi
2018-10-29Merge PR #8812: [ssreflect] Better use of CoqlibEnrico Tassi
2018-10-29[gramlib] Wrap `Gramlib`.Emilio Jesus Gallego Arias
This introduces a bit of noise in the Dune files but for now I think it is the best way to do it.
2018-10-29[gramlib] Cleanup, remove unused parsing infrastructure.Emilio Jesus Gallego Arias
We remove the functional and backtracking parsers as they are not used in Coq.
2018-10-29[camlp5] Fix warnings, switch Coq to vendored library.Emilio Jesus Gallego Arias
2018-10-29[camlp5] Automatic conversion from revised syntax + parsersEmilio Jesus Gallego Arias
`for i in *; do camlp5r pr_o.cmo $i > ../gramlib.auto/$i; done`
2018-10-29[gramlib] Original Import from Camlp5 repos.Emilio Jesus Gallego Arias
2018-10-28Merge PR #8827: Revert "[ci] Pin CI_REF to plugin_tutorial to use not yet ↵Emilio Jesus Gallego Arias
merged commit."
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 14:10:13 +0000