aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-10-19Merge PR #13192: Fix algebraic on the right when using bidi hintscoqbot-app[bot]
2020-10-16Merge PR #13195: Add support for "typeclasses eauto bfs <int_or_var_opt>"Pierre-Marie Pédrot
2020-10-16Merge PR #13196: For "Typeclasses eauto", search depth should be a natural, n...Pierre-Marie Pédrot
2020-10-15Merge PR #12925: [declare] Fix types of mutual lemmas when using Admitted.coqbot-app[bot]
2020-10-15Merge PR #13098: Deprecating wit_var to the benefit of its synonymous wit_hypPierre-Marie Pédrot
2020-10-15Merge PR #13181: Guard unify_leq_delay calls in TypingPierre-Marie Pédrot
2020-10-15Merge PR #13140: Documenting Set Printing Goal Names + a small goal display fixcoqbot-app[bot]
2020-10-15Merge PR #13144: Closes #13142: more standardized pretty-printing of Coq recordscoqbot-app[bot]
2020-10-15[declare] Fix types of mutual lemmas when using Admitted.Emilio Jesus Gallego Arias
2020-10-14For "Typeclasses eauto", search depth should be a natural, not anJim Fehrle
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
2020-10-14Deprecating wit_var to the benefit of its synonymous wit_hyp.Hugo Herbelin
2020-10-14Merge PR #13147: Use OCaml floating-point operations on 64 bits archcoqbot-app[bot]
2020-10-13Merge PR #13172: Fix #13169: vm_compute has existential crisis.coqbot-app[bot]
2020-10-13Merge PR #13099: Locating pattern identifiers (?id) by default at parsing tim...Pierre-Marie Pédrot
2020-10-12Merge PR #13185: Add missing ";" in Record grammarcoqbot-app[bot]
2020-10-12Add missing ";" in record grammarJim Fehrle
2020-10-12Merge PR #13156: Store the resolver of required modules as functor parameters...coqbot-app[bot]
2020-10-12Merge PR #12874: Add a "Show Proof Diffs" message to the XML protocolcoqbot-app[bot]
2020-10-12Merge PR #13163: [printing] make detyping resilient to "let x : _ := t in"coqbot-app[bot]
2020-10-12Merge PR #13175: [ci] elpi 1.11.4coqbot-app[bot]
2020-10-12Catch more errors in Unification.abstract_list_allGaëtan Gilbert
2020-10-12Guard unify_leq_delay calls in TypingGaëtan Gilbert
2020-10-12Merge PR #12449: Minimize Prop <= i to i := Setcoqbot-app[bot]
2020-10-12Merge PR #12950: Notations: reworking the treatment of only-parsing and only-...coqbot-app[bot]
2020-10-12elpi 1.11.4Enrico Tassi
2020-10-11Fix #13169: vm_compute has existential crisis.Pierre-Marie Pédrot
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
2020-10-10Splitting ssrbool's multi-printing notations into parsing and printing.Hugo Herbelin
2020-10-10Notation.ml: Move interpretation_eq earlier for future use.Hugo Herbelin
2020-10-10Print Scope & cie: Add parentheses around notation interpretation.Hugo Herbelin
2020-10-10Prim.pattern_ident takes a location and its synonymous pattern_identref is de...Hugo Herbelin
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 miss...Hugo Herbelin
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]
2020-10-09Add an XML message for "Show Proof Diffs"Jim Fehrle
2020-10-09Update pretyping/detyping.mlEnrico Tassi
2020-10-09Merge PR #13088: [stm] move par: to comTacticcoqbot-app[bot]
2020-10-09overlay for mtac2Enrico Tassi
2020-10-09[stm] move par: implementation to vernac/comTactic and stm/partacEnrico Tassi
2020-10-09Merge PR #13143: Drop misleading argument of Pp.h boxcoqbot-app[bot]
2020-10-09improve commentEnrico Tassi
2020-10-09[bench] Dump the vo size difference.Pierre-Marie Pédrot
2020-10-09overlay for minim-prop-tosetGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 22:44:47 +0000