aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-10-09Modify Bool/Sumbool.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify ZArith/Zorder.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify setoid_ring/Ring_polynom.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify ZArith/BinInt.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZBits.v to compile with -mangle-namesJasper Hugunin
As before, add a `bitwise as` tactic notation.
2020-10-08Modify Numbers/Integer/Abstract/ZLcm.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZGcd.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZDivFloor.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZDivTrunc.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZPow.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZParity.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZSgnAbs.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZMaxMin.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZMulOrder.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZAddOrder.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZAdd.v to compile with -mangle-namesJasper Hugunin
All that really needed to be done was add an explicit intro before nzinduct, but all the issues in this file could be fixed by moving n m p before the colon, and I couldn't stop my self.
2020-10-08Merge PR #12949: When a notation is only parsing, do not attach to it a ↵coqbot-app[bot]
specific format. Reviewed-by: ejgallego
2020-10-08Merge PR #13159: update for Iris build system changescoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-10-08update for Iris build system changesRalf Jung
2020-10-08Merge PR #13128: Define a new type instance_flag instead of using [unit option]Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-07Merge PR #13152: Algorithmically faster implementation of ↵coqbot-app[bot]
Evarconv.apply_on_subterm Reviewed-by: mattam82
2020-10-07Merge PR #13115: Derive Inversion does not allow leftover evarsPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-07Merge PR #13119: Fix retyping anomaly in rewritePierre-Marie Pédrot
Reviewed-by: ppedrot
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 21:30:49 +0000