aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-10-02Cleanup rewrite.mlGaëtan Gilbert
Remove unused arguments and commented code
2020-10-02Merge PR #13106: Remove the forward class hint feature.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-10-01Merge PR #13108: Getting rid of temerarious EConstr.to_constr in Himsgcoqbot-app[bot]
Reviewed-by: ejgallego
2020-10-01Merge PR #13114: Reimplement Admit Obligations using standard Admitted codecoqbot-app[bot]
Reviewed-by: ejgallego
2020-10-01Merge PR #13116: interp_context_evars: removed unused [shift] argumentcoqbot-app[bot]
Reviewed-by: ejgallego
2020-10-01Merge PR #13123: Fix combining uniform parameters and mutual inductives.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-09-30Fix combining uniform parameters and mutual inductives.Jasper Hugunin
2020-09-30Merge PR #13021: Almost fully moving funind to new proof enginePierre-Marie Pédrot
Reviewed-by: ppedrot
2020-09-30Merge PR #13032: More precise information when unification fails because of ↵Pierre-Marie Pédrot
incompatible candidates Reviewed-by: ppedrot
2020-09-30Further simplification of the typeclass registration API.Pierre-Marie Pédrot
2020-09-30Remove the forward class hint feature.Pierre-Marie Pédrot
It was not documented, not properly tested and thus likely buggy. Judging from the code alone I spotted already one potential bug. Further more it was prominently making use of the infamous "arbitrary term as hint" feature. Since the only user in our CI seems to be a math-classes file that introduced the feature under a claim of "cleanup", I believe we can safely remove it without anyone noticing.
2020-09-30interp_context_evars: removed unused [shift] argumentGaëtan Gilbert
Became unused in e034b4090ca45410853db60ae2a5d2f220b48792
2020-09-30Reimplement Admit Obligations using standard Admitted codeGaëtan Gilbert
Fix #13109
2020-09-29Merge PR #13111: Small document fixes.coqbot-app[bot]
Reviewed-by: jfehrle
2020-09-29Applying ocamlformat.Hugo Herbelin
2020-09-29Almost fully moving funind to new proof engine.Hugo Herbelin
2020-09-29Adding a few tacticals for the purpose of porting funind to new proof engine.Hugo Herbelin
2020-09-30Wf.v defines Fix_eq, not fix_eq.Tanaka Akira
A commit at 2003-03-13 changed the lemma name. https://github.com/coq/coq/commit/cb1ae314411d78952062e5092804b85d981ad6e1
2020-09-30Type{i} should be Type(i).Tanaka Akira
2020-09-29Merge PR #13101: Reduce nitpick_ignore list a little.Clément Pit-Claudel
2020-09-29Merge PR #13097: Modify how quotations handle whole sentences.coqbot-app[bot]
Reviewed-by: gares
2020-09-29Merge PR #13039: Lint stdlib with -mangle-names #3coqbot-app[bot]
Reviewed-by: anton-trunov
2020-09-28Merge PR #12946: Fixes part 1 of #12908: undetected collision involving a ↵coqbot-app[bot]
lonely notation at printing time. Reviewed-by: ejgallego Ack-by: maximedenes
2020-09-28Getting rid of temerarious EConstr.to_constr in Himsg.Hugo Herbelin
2020-09-28Merge PR #13105: [nix] CI script wrapper now requires Pythoncoqbot-app[bot]
Reviewed-by: vbgl
2020-09-28Merge PR #13053: [lib] make canonical_path_name always absolute (fix #13031)Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-09-28More precise information when unification fails because of incompatible ↵Hugo Herbelin
candidates. We also show the incompatible contender. Ideally, we should also remember the source of the other contender.
2020-09-28CI script wrapper now requires PythonMaxime Dénès
2020-09-27Avoid lookup up too many characters.Guillaume Melquiond
This would cause issues in noninteractive mode. For example, when using Drop, the first character of the OCaml code would be read by Coq's REPL instead of OCaml's REPL. The peek_string function is quite inefficient, since the Stream module does not provide any good function to lookup arbitrary characters (or to push back characters).
2020-09-27Reduce nitpick_ignore list a little.Théo Zimmermann
2020-09-27Recognize only ":{{" as a sentence-gobbling quotation.Guillaume Melquiond
2020-09-27Make "xxx:{{" always start a quotation, whether registered or not.Guillaume Melquiond
This commit also prevents quotations using "(" and "[" from gobbling sentences. As a consequence, dynamically-registered quotations can no longer modify where Coq sentences stop.
2020-09-25Merge PR #12999: More improvements in locating tactic errorscoqbot-app[bot]
Reviewed-by: ppedrot Reviewed-by: ejgallego
2020-09-24Merge PR #12894: Modify bytecode representation of closures to please OCamls ↵coqbot-app[bot]
GC (fix #12636). Reviewed-by: maximedenes Ack-by: bgregoir Ack-by: proux01
2020-09-24Merge PR #13077: Fix issue #13065 - Windows CI brokencoqbot-app[bot]
Reviewed-by: Zimmi48
2020-09-23Fix issue #13065 - Windows CI brokenMichael Soegtrop
2020-09-23Merge PR #12977: Statically ensure that only polymophic hint terms come with ↵coqbot-app[bot]
a context. Reviewed-by: mattam82
2020-09-23Merge PR #13073: A temporary fix of #13018 and #12775 for branch 8.12 (bis)coqbot-app[bot]
Reviewed-by: ejgallego
2020-09-23Merge PR #13028: Fixes #9716 and #13004: don't drop the qualifier of ↵Pierre-Marie Pédrot
quotations at printing time Reviewed-by: ppedrot
2020-09-23Merge PR #12847: Tactics inversion and replace work with eq in typePierre-Marie Pédrot
Reviewed-by: ppedrot
2020-09-22Merge PR #13061: fix build:quick and build:base+async artifactscoqbot-app[bot]
Reviewed-by: Zimmi48
2020-09-22Merge PR #13067: Setting default value for Display Parentheses off in CoqIDEcoqbot-app[bot]
Reviewed-by: ejgallego
2020-09-22Merge PR #12960: Fixes #9403 and #10803: missing flattening of nested ↵coqbot-app[bot]
applications in notations Reviewed-by: ejgallego Ack-by: maximedenes
2020-09-22Adding change log for #12794 and #13067.Hugo Herbelin
2020-09-22Setting default value for Display Parentheses off in CoqIDE.Hugo Herbelin
2020-09-22Add overlay for Equations.Hugo Herbelin
2020-09-22Adding change log for #13028.Hugo Herbelin
2020-09-22Fixes #9716, #13004: don't drop the qualifier of quotations at printing time.Hugo Herbelin
2020-09-22Use the closure tag for accumulators.Guillaume Melquiond
The first field of accumulators points out of the OCaml heap, so using closures instead of tag-0 objects is better for the GC. Accumulators are distinguished from closures because their code pointer necessarily is the "accumulate" address, which points to an ACCUMULATE instruction.
2020-09-22Use the same memory layout as closures for accumulators.Guillaume Melquiond
That way, accumulators again can be used directly as execution environments by the bytecode interpreter. This fixes the issue of the first argument of accumulators being dropped when strongly normalizing.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 13:13:12 +0000