aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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-29Fix for bug #8848Matthieu Sozeau
2018-10-29Merge PR #8751: Rename checker/{main->coqchk}Pierre-Marie Pédrot
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-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."
2018-10-27Merge PR #8741: [typeclasses] functionalize typeclass evar handlingPierre-Marie Pédrot
2018-10-26[typeclasses] functionalize typeclass evar handlingMatthieu Sozeau
This avoids all the side effects associated with the manipulation of an unresolvable flag. In the new design: - The evar_map stores a set of evars that are candidates for typeclass resolution, which can be retrieved and set. We maintain the invariant that it always contains only undefined evars. - At the creation time of an evar (new_evar), we classify it as a potential candidate of resolution. - This uses a hook to test if the conclusion ends in a typeclass application. (hook set in typeclasses.ml) - This is an approximation if the conclusion is an existential (i.e. not yet determined). In that case we register the evar as potentially a typeclass instance, and later phases must consider that case, dropping the evar if it is not a typeclass. - One can pass the ~typeclass_candidate:false flag to new_evar to prevent classification entirely. Typically this is for new goals which should not ever be considered to be typeclass resolution candidates. - One can mark a subset of evars unresolvable later if needed. Typically for clausenv, and marking future goals as unresolvable even if they are typeclass goals. For clausenv for example, after turing metas into evars we first (optionally) try a typeclass resolution on the newly created evars and only then mark the remaining newly created evars as subgoals. The intent of the code looks clearer now. This should prevent keeping testing if undefined evars are classes all the time and crawling large sets when no typeclasses are present. - Typeclass candidate evars stay candidates through restriction/evar-evar solutions. - Evd.add uses ~typeclass_candidate:false to avoid recomputing if the new evar is a candidate. There's a deficiency in the API, in most use cases of Evd.add we should rather use a: `Evd.update_evar_info : evar_map -> Evar.t -> (evar_info -> evar_info) -> evar_map` Usually it is only about nf_evar'ing the evar_info's contents, which doesn't change the evar candidate status. - Typeclass resolution can now handle the set of candidates functionally: it always starts from the set of candidates (and not the whole undefined_map) and a filter on it, potentially splitting it in connected components, does proof search for each component in an evar_map with an empty set of typeclass evars (allowing clean reentrancy), then reinstates the potential remaining unsolved components and filtered out typeclass evars at the end of resolution. This means no more marking of resolvability/unresolvability everywhere, and hopefully a more efficient implementation in general. - This is on top of the cleanup of evar_info's currently but can be made independent. [typeclasses] Fix cases.ml: none of the new_evars should be typeclass candidates Solve bug in inheritance of flags in evar-evar solutions. Renaming unresolvable to typeclass_candidate (positive) and fix maybe_typeclass_hook
2018-10-26Fix overlay for this extension of the PR. To be removed.Matthieu Sozeau
2018-10-26PR 8671: Add overlay for plugin-tutorialMatthieu Sozeau
2018-10-26Cleanup evar_extra: remove evar_info's store and add maps to evar_mapMatthieu Sozeau
2018-10-26Merge PR #8684: Remove a few circumvolutions around parameters of inductive ↵Gaëtan Gilbert
entries
2018-10-26Add record names to multiple records error messageTej Chajed
2018-10-26Correctly report non-projection fields in recordsTej Chajed
Fixes #8736.
2018-10-26[libobject] Move object_name next to object definition.Emilio Jesus Gallego Arias
`object_name` is a particular choice of the implementation of `Liboject`, thus it makes sense to tie it to that particular module. This may prove useful in the future as we may want to modify object naming.
2018-10-26Merge PR #8687: Mini reorganization type of global constr of globalPierre-Marie Pédrot
2018-10-26Merge PR #8814: Comment Environ.set_universesMaxime Dénès
2018-10-26Revert "[ci] Pin CI_REF to plugin_tutorial to use not yet merged commit."Gaëtan Gilbert
This reverts commit df69c44af03f2587b3f1706a805d0e2728c1f1dc. Should be merged before any PR with plugin tutorial overlays, or we can just merge the vendor PR instead.
2018-10-26Merge PR #8803: Fix issue #8800 (gtk warning about ↵Pierre-Marie Pédrot
gtk_scrolled_window_add_with_viewport)
2018-10-26Merge PR #8804: Fix issue #8801 (uncaught Not_found after F1 sequence in coqide)Pierre-Marie Pédrot
2018-10-26Overlay for kernel entries changeMaxime Dénès
2018-10-26Remove a few circumvolutions around parameters of inductive entriesMaxime Dénès
2018-10-26Merge PR #8744: [dune] Compile debug and checker printers.Gaëtan Gilbert
2018-10-26Merge PR #8753: [build] Refactoring of config lib and ocamldebug tweaks.Gaëtan Gilbert
2018-10-26Merge PR #8821: [default.nix] Update to dune 1.4.Vincent Laporte
2018-10-26Merge PR #8777: Move side-effects into Safe_typingMaxime Dénès
2018-10-26Merge PR #8707: Separate cache representation between CClosure and CBVMaxime Dénès
2018-10-26Merge PR #7186: Moving `fold_constr_with_full_binders` to a placeMaxime Dénès
2018-10-26[default.nix] Clean-up: use camlp5 instead of synonymous camlp5_strict.Théo Zimmermann
2018-10-25[default.nix] Update to dune 1.4.Théo Zimmermann
2018-10-25Merge PR #8762: [dune] [opam] Move to OPAM 2.0Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 15:13:41 +0000