| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
This fixes [bug #5019](https://coq.inria.fr/bugs/show_bug.cgi?id=5019),
"[zify] loops on dependent types"; before, we would see a `Z.of_nat (S
?k)` which could not be turned into `Z.succ (Z.of_nat k)`, add a
hypothesis of the shape `0 <= Z.of_nat (S k)`, turn that into a
hypothesis of the shape `0 <= Z.succ (Z.of_nat k)`, and loop forever on
this.
This may not be the "right" fix (there may be cases where `zify` should
succeed where it still fails with this change), but this is a pure
bugfix in the sense that the only places where it changes the behavior
of `zify` are the places where, previously, `zify` looped forever.
|
| |
|
|
|
|
|
|
|
|
|
| |
Two issues in one:
- some focused_simpl were called on the wrong locations
- some focused_simpl were done on whole equations
In the two cases, this could be bad if "simpl" goes too far
with respect to what omega expects: later calls to "occurrence"
might fail. This may happen for instance if an atom isn't a variable,
but a let-in (b:=5:Z in the example).
|
| | |
|
| | |
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| | |
This way, after we merge PR#220, scripts can be fixed in a way that is
compatible with the 8.6 and trunk branches.
|
| |/
|
|
|
|
| |
Fixes [Coq bug #5372](https://coq.inria.fr/bugs/show_bug.cgi?id=5372)
"Anomaly: Not a valid information when defining mutual fixpoints that
are not mutual with Function".
|
| |
|
|
| |
This is needed to fix `Declare ML Module "ltac_plugin".
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
A double call to pp_module_type inside Ocaml.pp_specif was
causing an complexity blowup when pretty-printing heavily modular
extracted code.
I wasn't able to figure out why this double call is there. It could
be the leftover of some intermediate work in 2007 before commit 350398eae
(which introduced global printing phases Pre/Impl/Intf).
Anyway I'm reasonably sure that today these two pp_module_type calls produce
the exact same pretty-printed signature (even if there's a large bunch of
imperative states around). Moreover, this duplicated signature is actually
slightly wrong: when we alias a module M with a unambiguous name like Coq__123,
the type of Coq__123 should not be an exact copy of the type of M, but rather
a "strengthened" version of it (with equality between inductive types).
So the best solution is now to use this funny feature of OCaml introduced in 3.12 :
module Coq__123 : module type of struct include M end
This "module type of struct include" is slightly awkward, but short, correct,
and trivial to produce :-). And I doubt anybody will object to the (rare) use
of some 3.12 features in extracted code of 2017...
|
| | |
|
| | |
|
| | |
|
| | |
|
| |\
| |
| |
| | |
Was PR#331: Solve_constraints and Set Use Unification Heuristics
|
| |\ \
| | |
| | |
| | | |
Was PR#319: More error tagging, try to fix bug 5135
|
| |\ \ \
| | | |
| | | |
| | | | |
Was PR#334: Fix bug 5031 : should not be an anomaly
|
| | | | |
| | | |
| | | |
| | | | |
not an anomaly
|
| |/ / / |
|
| | |/
|/|
| |
| |
| | |
reconsider_conv_pbs -> reconsider_unif_constraints
consider_remaining_unif_problems -> solve_unif_constraints_with_heuristics
|
| | | |
|
| |/
|
|
|
|
|
|
| |
The current tag system in `Pp` is generic, which implies we must choose
a tagging function when calling a printer.
For console printing there is a single choice, thus this commits adds it
a few missing cases.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
This fixes the stack overflow part of the bug, even if the tactic is still quite
slow. The offending functions have been written in a tail-recursive way.
|
| |
|
|
| |
One of them revealed a true bug.
|
| |
|
|
| |
esprit d'escalier : is now also fixed for R
|
| |
|
|
|
| |
The computed proof term is now more explicit exact (__arith P1 ... Pn X1 ... Xm)
instead of apply (__arith P1 ... Pn) which unification could fail.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| | |
- Assert a purely arihtmetic sub-goal that is proved independently by reflexion.
(This reduces the stress on the conversion test)
- Does not use 'abstract' anymore (more natural proof-term)
- Fix a parsing bug (certain terms in Prop where not recognized)
|
| | | |
|
| |\| |
|
| | | |
|
| | |
| |
| |
| | |
If 'abstract' fails e.g. if there are existentials. The tactic runs an abstract-free alternative.
|
| | |
| |
| |
| |
| |
| |
| | |
(Fixed #4985)
Lqa.v defines the tactics lra and nra working over Q.
Lra.v defines the tactics lra and nra working over R.
|
| | |
| |
| |
| |
| |
| | |
csdp.cache -> .csdp.cache
lia.cache -> .lia.cache
nlia.cache -> .nia.cache
|
| | | |
|
| | | |
|
| | | |
|
| |\| |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | | |
we use a hashtable to reduce the complexity of creating
a duplicate-free list.
|
| | |/
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
the function in_ideal of ideal.ml supposes the list of polynomials
does not contain zero and is duplicate free.
I force this invariant in the call of in_ideal in nsatz.ml4
the function clean_pol returns the reduced list plus a list of
booleans that indicates which polynomials have been deleted
the function expand_pol translates back the certificate of
the reduced to list to the complete list thanks to the list
of booleans.
The fix is quadratic with respect to the input list which should
be ok for reasonable usage of nsatz.
If there is some performance issue we could improve the in_pol
function.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
This reverts commit b2f8f9edd5c1bb0a9c8c4f4b049381b979d3e385, reversing
changes made to da99355b4d6de31aec5a660f7afe100190a8e683.
Hugo asked for more discussion on this topic, and it was not in the roadmap. I
merged it prematurely because I thought there was a consensus. Also, I missed
that it was changing coq_makefile. Sorry about that.
|
| | |
| |
| |
| |
| |
| |
| |
| | |
changing
set (x := val)
into
let x := fresh "x" in
set (x := val)
|
Jason Gross
Pierre Letouzey
Julien Forest
Maxime Dénès
Tej Chajed
Emilio Jesus Gallego Arias
Enrico Tassi
Hugo Herbelin
Guillaume Melquiond
Yves Bertot
Matthieu Sozeau
Pierre-Marie Pédrot
Frédéric Besson
thery