aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-10-19Merge PR #13197: Require at least one reference for Typeclasses ↵coqbot-app[bot]
Opaque/Transparent Reviewed-by: SkySkimmer
2020-10-19Merge PR #13194: Add flag -open Gramlib so that merlin works in gramlib with ↵coqbot-app[bot]
make Reviewed-by: SkySkimmer
2020-10-19Merge PR #13204: Consistent indentation + a few bullets in RIneq.v.coqbot-app[bot]
Reviewed-by: silene
2020-10-19Merge PR #13151: Remove the compare_graph field from the conversion API.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-10-19Merge PR #13166: Fixes #13165: implicit arguments in defined fields of ↵coqbot-app[bot]
record types not taken into account Reviewed-by: SkySkimmer
2020-10-19Merge PR #13207: Use list notation in examples referenced by "nsatz" ↵coqbot-app[bot]
documentation Reviewed-by: Zimmi48
2020-10-19Adding change log for #13092.Hugo Herbelin
2020-10-19Addressing parsing part #13078.Hugo Herbelin
We don't give sense to pattern/binders in leftmost position.
2020-10-19Fixing printing part of #13078 (anomaly with binding notations in patterns).Hugo Herbelin
We prevent notations involving binders (i.e. names or patterns) to be used for printing in "match" patterns. The computation is done in "has_no_binders_type", controlling uninterpretation.
2020-10-19Merge PR #13192: Fix algebraic on the right when using bidi hintscoqbot-app[bot]
Reviewed-by: gares
2020-10-16Use list notation in nsatz examples referenced in the docJim Fehrle
2020-10-16Merge PR #13195: Add support for "typeclasses eauto bfs <int_or_var_opt>"Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-16Merge PR #13196: For "Typeclasses eauto", search depth should be a natural, ↵Pierre-Marie Pédrot
not an integer Reviewed-by: ppedrot
2020-10-16Overlay for elpi.Hugo Herbelin
2020-10-15Support "Solve Obligations of <ident>" optionJim Fehrle
2020-10-16Add change log for #13166.Hugo Herbelin
2020-10-16Fixes/enhancements with local definitions in records.Hugo Herbelin
Fixes implicit arguments from the body of a defined field not taken into account. Get (a bit) more information for detection of SProp relevance in implicitly-typed defined field. (It should be done at the very end of the inference phase, though, because some evars may not yet be instantiated.)
2020-10-16Generalizing and exporting interp_assumption/interp_definition.Hugo Herbelin
This shall be for Record fields consumption.
2020-10-15Merge PR #12925: [declare] Fix types of mutual lemmas when using Admitted.coqbot-app[bot]
Reviewed-by: herbelin Ack-by: SkySkimmer
2020-10-15Consistent indentation + a few bullets in RIneq.v.Hugo Herbelin
2020-10-15Report a useful error for dependent destructionTej Chajed
Similar to `dependent induction`, report an error message for `dependent destruction` saying that importing `Coq.Program.Equality` is required, rather than failing at parsing time. This is a small extension of #605 to cover dependent destruction as well. Here I also put in some tests.
2020-10-15Merge PR #13098: Deprecating wit_var to the benefit of its synonymous wit_hypPierre-Marie Pédrot
Reviewed-by: ejgallego Reviewed-by: gares Ack-by: jfehrle Reviewed-by: ppedrot
2020-10-15Merge PR #13181: Guard unify_leq_delay calls in TypingPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-15Merge PR #13140: Documenting Set Printing Goal Names + a small goal display fixcoqbot-app[bot]
Reviewed-by: ejgallego Reviewed-by: Zimmi48
2020-10-15Merge PR #13144: Closes #13142: more standardized pretty-printing of Coq recordscoqbot-app[bot]
Reviewed-by: ejgallego Ack-by: SkySkimmer
2020-10-15[declare] Fix types of mutual lemmas when using Admitted.Emilio Jesus Gallego Arias
We fix a clear coding mistake in 79bcf1c0a22e736c4e2cae3460c35b3d9fca9aa0 that forgot to update the type of the parameter entry when saving mutual definitions without a body. We follow the solution suggested by Hugo Herbelin and drop the type used in `start_proof`. Note the duplication here indeed. Fixes #12895 Co-authored-by: Hugo Herbelin <Hugo.Herbelin@inria.fr>
2020-10-15Require at least one reference for Typeclasses Opaque/TransparentJim Fehrle
(zero references is currently a no-op)
2020-10-14For "Typeclasses eauto", search depth should be a natural, not anJim Fehrle
integer
2020-10-14Add support for "typeclasses eauto bfs <int_or_var_opt>Jim Fehrle
2020-10-14Add flag -open Gramlib so that merlin works in gramlib with make.Hugo Herbelin
2020-10-14[build] [native] Don't assume installed native libraries are in custom ↵Emilio Jesus Gallego Arias
output path In #11581 we introduced the `-native-output-dir` option to allow the build system to redirect the output of the native compiler. Unfortunately that patch also modified the default loadpath, which is now buggy if a library with native is installed. We thus revert the change to the loadpath handling, so for now additional native build paths have to be passed with `-nI`. Note that unfortunately in `link_library` we don't know if the required library is coming from the build dir or from an installed dir, as this information is generated from `Require` statements in `Library.get_used_load_paths`. We thus check and give priority to files in the build location. As to make the patch backportable I introduced an extra `stat` system call which should not be problematic as the cache will be hot for the second call. An alternative would be actually to modify loadpath compilation in `call_compiler` so both include paths would be added if `output_dir` is not the default, however that seems pretty noisy given the large path set returned by `!get_load_paths`.
2020-10-14Fix algebraic on the right when using bidi hintsGaëtan Gilbert
Fix #12970 We can't recover the expected type of the post bidi argument by retyping because the hole may be filled by something in which case retyping can produce algebraic universes.
2020-10-14Fix anomaly when importing a functorGaëtan Gilbert
Fix #13162
2020-10-14Deprecating wit_var to the benefit of its synonymous wit_hyp.Hugo Herbelin
Note: "hyp" was documented in Ltac Notation chapter but "var" was not.
2020-10-14Merge PR #13147: Use OCaml floating-point operations on 64 bits archcoqbot-app[bot]
Reviewed-by: erikmd Reviewed-by: silene
2020-10-13Merge PR #13172: Fix #13169: vm_compute has existential crisis.coqbot-app[bot]
Reviewed-by: silene
2020-10-13Merge PR #13099: Locating pattern identifiers (?id) by default at parsing ↵Pierre-Marie Pédrot
time and use location in some typing error messages Reviewed-by: ppedrot
2020-10-12Merge PR #13185: Add missing ";" in Record grammarcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-10-12Add missing ";" in record grammarJim Fehrle
2020-10-12Merge PR #13156: Store the resolver of required modules as functor ↵coqbot-app[bot]
parameters in safe_env Reviewed-by: herbelin
2020-10-12Merge PR #12874: Add a "Show Proof Diffs" message to the XML protocolcoqbot-app[bot]
Reviewed-by: herbelin Ack-by: gares Ack-by: ejgallego
2020-10-12Merge PR #13163: [printing] make detyping resilient to "let x : _ := t in"coqbot-app[bot]
Reviewed-by: herbelin Ack-by: SkySkimmer
2020-10-12Merge PR #13175: [ci] elpi 1.11.4coqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: MSoegtropIMC
2020-10-12Check types when converting irrelevant terms in old unificationGaëtan Gilbert
Fixes probably many strange issues such as the example in #13171
2020-10-12Catch more errors in Unification.abstract_list_allGaëtan Gilbert
This improves the error message on the example for #13171, however we may question whether there should be an error at all.
2020-10-12Guard unify_leq_delay calls in TypingGaëtan Gilbert
Fix #13171
2020-10-12Respect Print Universes when printing primitive arraysGaëtan Gilbert
2020-10-12Merge PR #12449: Minimize Prop <= i to i := Setcoqbot-app[bot]
Reviewed-by: mattam82 Ack-by: Janno Ack-by: gares
2020-10-12Merge PR #12950: Notations: reworking the treatment of only-parsing and ↵coqbot-app[bot]
only-printing notations Reviewed-by: SkySkimmer
2020-10-12Automatically merge overlays with most recent upstream versionGaëtan Gilbert
This avoids the need to rebase the overlay when nothing has changed.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 11:37:58 +0000