aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-10-07Explicitly pass around a state in Evarconv.second_order_matching.Pierre-Marie Pédrot
I know higher-order mutable state shared across call sites is a staple of Matthieu's style, but it is a footgun begging to be abused.
2020-10-07Algorithmically faster implementation of Evarconv.apply_on_subterm.Pierre-Marie Pédrot
Instead of repeatedly checking for evars to appear in a term, we perform the search in one single pass. This slowdown was observed in fiat-crypto. This is still a naive algorithm though, since we recompute the set of evars for each subterm. This is thus quadratic.
2020-10-06Merge PR #13141: Document the removal of forward class hints.coqbot-app[bot]
Reviewed-by: jfehrle Ack-by: ppedrot
2020-10-06Use OCaml floating-point operations on 64 bits archPierre Roux
C functions were used for floating-point arithmetic operations, by fear of double rounding that could happen on old x87 on 32 bits architecture. This commit uses OCaml floating-point operations on 64 bits architectures. The following snippet is made 17% faster by this commit. From Coq Require Import Int63 BinPos PrimFloat. Definition foo n := let eps := sub (next_up one) one in Pos.iter (fun x => add x eps) two n. Time Eval native_compute in foo 1000000000.
2020-10-06Define a new type instance_flag instead of using [unit option]Gaëtan Gilbert
2020-10-05Document the removal of forward class hints.Théo Zimmermann
2020-10-04Merge PR #13096: Drop prefixes from non-terminal names, e.g. "constr:constr" ↵coqbot-app[bot]
-> "constr" Reviewed-by: herbelin Ack-by: Zimmi48
2020-10-04Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."Jim Fehrle
2020-10-03Merge PR #12985: Remove ocamlformat from the linter and the pre-commit hook.coqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: gares Reviewed-by: maximedenes Reviewed-by: Matafou Ack-by: ejgallego
2020-10-02Merge PR #13125: More details in the documentation of native arrayscoqbot-app[bot]
Reviewed-by: jfehrle Ack-by: Blaisorblade Ack-by: herbelin
2020-10-02More details in the documentation of native arraysVincent Semeria
Update doc/sphinx/language/core/primitive.rst Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com> Add persistent data structure Update doc/sphinx/language/core/primitive.rst Co-authored-by: Hugo Herbelin <herbelin@users.noreply.github.com> Update doc/sphinx/language/core/primitive.rst Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com> Update doc/sphinx/language/core/primitive.rst Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-10-02Merge PR #13054: {new,setoid_}ring -> ringcoqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: jfehrle
2020-10-02{new,setoid_}ring -> ringMaxime Dénès
I believe this renaming makes it easier for new contributors to discover the code of `ring`.
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-30Fix retyping anomaly in rewriteGaëtan Gilbert
Fix #13045 Also make sure future anomalies won't be fed to tclzero. Instead of retyping with lax:true we may question why we produce an ill-typed term in decompose_app_rel: in the | App (f, [|arg|]) -> case we produce `fun x y : T => bla x y` but we have no assurance that the second argument of `bla` should have type `T`.
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-30Derive Inversion does not allow leftover evarsGaëtan Gilbert
Fix #12917
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-28Put type-in-type flag in ugraph.Gaëtan Gilbert
Fix #13086.
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-28Document the ocamlformat changes.Pierre-Marie Pédrot
2020-09-28Remove the linter ocamlformat pass.Pierre-Marie Pédrot
2020-09-28Remove the ocamlformat git hook.Pierre-Marie Pédrot
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 22:22:15 +0000