aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-10-21Merge PR #13222: Bench: move variables to the scriptPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-21Merge PR #13118: [type classes] Simplify cl_contextPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-21Merge PR #13201: Report a useful error for dependent destructionPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-21Merge PR #12955: Reroot primitive arrays on accesscoqbot-app[bot]
Reviewed-by: maximedenes
2020-10-20Merge PR #13214: Better message for doc_grammar; avoid an infinite SPLICE loopcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-10-20Merge PR #12648: [zify] support for int63coqbot-app[bot]
Reviewed-by: vbgl Ack-by: JasonGross Ack-by: jfehrle Ack-by: silene
2020-10-20Merge PR #13180: Respect Print Universes when printing primitive arrayscoqbot-app[bot]
Reviewed-by: herbelin
2020-10-20[zify] Use flag for Z.to_euclidean_division_equations.Frédéric Besson
Update doc/sphinx/addendum/micromega.rst Co-authored-by: Jason Gross <jasongross9@gmail.com> Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-10-20[zify] Add support for Int63.intFrédéric Besson
Update doc/sphinx/addendum/micromega.rst Co-authored-by: Jason Gross <jasongross9@gmail.com> Update theories/micromega/ZifyInt63.v Co-authored-by: Jason Gross <jasongross9@gmail.com>
2020-10-19Better message and avoid an infinite SPLICE loopJim Fehrle
2020-10-19Bench: move variables to the scriptGaëtan Gilbert
IMO it makes more sense this way, also it's more convenient if someone wants to run the script locally.
2020-10-19Merge PR #13208: Support "Solve Obligations of <ident>"coqbot-app[bot]
Reviewed-by: SkySkimmer
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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 15:53:38 +0000