aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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-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-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-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-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-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-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-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-12elpi 1.11.4Enrico Tassi
2020-10-11Fix #13169: vm_compute has existential crisis.Pierre-Marie Pédrot
We simply use evars instance in the right order while reading back VM values.
2020-10-10Adding change log for #12950.Hugo Herbelin
2020-10-10Documenting the new only-parsing only-printing model.Hugo Herbelin
2020-10-10New spacing/formatting in Locate Notation, Print Scopes, Print Visibility.Hugo Herbelin
2020-10-10Adding a warning in case a notation is used neither for parsing nor printing.Hugo Herbelin
2020-10-10Notations: reworking the treatment of only-parsing and only-printing notations.Hugo Herbelin
The (old) original model for notations was to associated both a parsing and a printing rule to a notation. Progressively, it become more and more common to have only parsing notations or even multiple expressions printed with the same notation. The new model is to attach to a given scope, string and entry at most one either only-parsing or mixed-parsing-printing rules + an arbitrarily many unrelated only-printing rules. Additionally, we anticipate the ability to selectively activate/deactivate each of those. This allows to fix in particular #9682 but also to have more-to-the-point warnings in case a notation overrides or partially overrides another one. Rules for importing are not changed (see forthcoming #12984 though). We also improve the output of "Print Scopes" so that it adds when a notation is only-parsing, only-printing, or deactivated, or a combination of those. Fixes #4738 Fixes #9682 Fixes part 2 of #12908 Fixes #13112
2020-10-10Splitting ssrbool's multi-printing notations into parsing and printing.Hugo Herbelin
This is in anticipation of a model with an explicit difference between a parsing-printing notation and the pair of only-parsing notation + only-printing notation.
2020-10-10Notation.ml: Move interpretation_eq earlier for future use.Hugo Herbelin
Also add optimisation of interpretation_eq.
2020-10-10Print Scope & cie: Add parentheses around notation interpretation.Hugo Herbelin
This is to be consistent with the use of parentheses in the syntax of Notation and to support a list of attribute afterwards.
2020-10-10Prim.pattern_ident takes a location and its synonymous pattern_identref is ↵Hugo Herbelin
deprecated.
2020-10-10Add location in existential variable names (CEvar/GEvar).Hugo Herbelin
2020-10-10Adding and using locations on identifiers in constr_expr where they were ↵Hugo Herbelin
missing.
2020-10-10Closes #13142 (more standardized pretty-printing of records).Hugo Herbelin
2020-10-10Merge PR #13164: [bench] Dump the vo size difference.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-10-09Add an XML message for "Show Proof Diffs"Jim Fehrle
Add menu item that uses this
2020-10-09Update pretyping/detyping.mlEnrico Tassi
Co-authored-by: Hugo Herbelin <herbelin@users.noreply.github.com>
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-06 03:30:29 +0000