aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-10-09Update pretyping/detyping.mlEnrico Tassi
Co-authored-by: Hugo Herbelin <herbelin@users.noreply.github.com>
2020-10-09Merge PR #13088: [stm] move par: to comTacticcoqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: ppedrot Reviewed-by: ejgallego
2020-10-09overlay for mtac2Enrico Tassi
2020-10-09[stm] move par: implementation to vernac/comTactic and stm/partacEnrico Tassi
The current implementation of par: is still in the STM, but is optional. If the STM does not take over it, it defaults to the implementation of in comTactic which is based on all: (i.e. sequential). This commit also moved the interpretation of a tactic from g_ltac to vernac/comTactic which is more appropriate. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-10-09Merge PR #13143: Drop misleading argument of Pp.h boxcoqbot-app[bot]
Reviewed-by: ejgallego Reviewed-by: silene
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
2020-10-09No bidirectionality when expected type for lambda is an evar.Gaëtan Gilbert
This fixes #12623 (bidirectionality breaks impredicativity).
2020-10-09Minimize Prop <= i to i := SetGaëtan Gilbert
Fix part of #8196, fix #12414 Replaces #9343
2020-10-09Merge PR #13087: Put type-in-type flag in ugraph.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-09Store the resolver of required modules as functor parameters in safe_env.Pierre-Marie Pédrot
The safe environment features two different sets of delta resolvers, one for module parameters and one for the actual body of the module being built. The purpose of this separations seems to have been to reduce the number of name equations being added to the environment, since the one from the parameters would already be present at instanciation time. Semantically, required modules behave like parameters in this respect, i.e. delta resolvers that come from modules dependend upon are guaranteed to be added when that module is actually required. As such, there is no need to store the quotient coming from the dependencies inside the vo file of a given library. Yet, the previous code would precisely do that, leading to a potential quadratic blowup in vo file size, similarly to the issue with vio files storing the whole chain of dependency. This patch fixes the issue simply by segregating those redundant constraints in the dedicated field, thus dropping them from the vo.
2020-10-09[printing] make detyping resilient to "let x : _ := t in"Enrico Tassi
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-08Add overlays for Coq-Equations, aac-tactics.Hugo Herbelin
2020-10-08Dropping the misleading int argument of Pp.h.Hugo Herbelin
An h-box inhibits the breaking semantics of any cut/spc/brk in the enclosed box. We tentatively replace its occurrence by an h or hv, assuming in particular that if the indentation is not 0, an hv box was intended.
2020-10-08Add a check of empty list of arguments in xmlprotocol where relevant.Hugo Herbelin
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-08Check complexity of primitive arrays.Guillaume Melquiond
2020-10-08Remove occurrences of Parray.reroot.Guillaume Melquiond
2020-10-08Reroot primitive arrays on access (fix #12947).Guillaume Melquiond
Semi-persistent arrays are supposed to have amortized O(1) complexity. This commit ensures it, without forcing the user to litter its functions with explicit calls to reroot. This commit also makes rerootk faster by carrying the array along the dependency chain rather than recomputing it at every step.
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-06Fixing redundant outputs when printing goals, especially in non-"pr_first" mode.Hugo Herbelin
Here is an example (see test output/goal_output.v for other examples): 2 subgoals, subgoal 1 (?Goal) subgoal 1 (?Goal) is: True subgoal 2 (?Goal0) is: True This is now: 2 subgoals subgoal 1 (?Goal) is: True subgoal 2 (?Goal0) is: True
2020-10-06Documenting option Set Printing Goal Name.Hugo Herbelin
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-06Remove unused is_class info from cl_contextGaëtan Gilbert
2020-10-06Implicit_quantifiers don't use precomputed is_class dataGaëtan Gilbert
Fix #13117 We alternatively could fix the generation of the data with Existing Class but I prefer moving towards removing it.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 10:43:20 +0000