| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
1) We now _assign_ the smallest possible arities to mutual inductive types
and eventually add leq constraints on the user given arities. Remove
useless limitation on instantiating algebraic universe variables with
their least upper bound if they have upper constraints as well.
2) Do not remove non-recursive variables when computing minimal levels of inductives.
3) Avoid modifying user-given arities if not necessary to compute the
minimal level of an inductive.
4) We correctly solve the recursive equations taking into account the
user-declared level.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
| |
maybe ca71714).
Goal 2=2+2.
match goal with |- (_ = ?c) => simpl c end.
was working in 8.4 but was failing in 8.5beta2.
Note: Changes in tacintern.ml are otherwise purely cosmetic.
|
| | |
|
| |
|
|
| |
Hence we reuse the ones in master.
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
Of course there is an exception to the previous commit.
Fail used to print even if silenced but loading a vernac file.
This behavior is useful only in tests, hence this flag.
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
test-suite.
|
| |
|
|
|
|
| |
Pretype_errors.PretypeError.
Instad of trying to print the exception, we raise it in the tactic monad.
|
| |
|
|
| |
negated into -native-compiler.
|
| |
|
|
|
|
| |
Internal error: Anomaly: Uncaught exception Not_found. Please report.
An evarmap was lost because of an unsound typing primitive.
|
| |
|
|
|
|
|
| |
the predicate, thus respecting the visual left-to-right top-down order
(see a45bd5981092).
This fixes CFGV.
|
| |
|
|
|
|
|
|
| |
The ~polyprop argument wasn't propagated properly anymore,
leading the extraction to try to operate on situations it cannot
handle (yet). Cf Table.error_singleton_become_prop for more details.
Regression test added.
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
preserving compatibility of subst after #4214 being solved.
|
| |
|
|
|
|
| |
Improving treatment of recursive equations compared to 8.4 (see test-suite).
Experimenting not to unfold local defs ever in subst.
(+ Slight simplification in checking reflexive equalities only once).
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
equalities in configurations like
x=y
x=z
===
P(x,y,z)
where it now produces
===
P(z,z,z)
In particular (equations are processed from most ancient to most recent).
Thanks to this, a "repeat subst" can just be a "subst" in List.v.
Incidentally: moved a nf_enter to enter in subst_one, since the latter
is normally called from other tactics having normalized evars.
|
| |
|
|
|
| |
Followup of: f7b29094fe7cc13ea475447bd30d9a8b942f0fef . In particular, re-closes #3593.
As a side effect, fixes an undiscovered bug of the `eq_constr` tactic which didn't consider terms up to evar instantiation.
|
| | |
|
| |
|
|
| |
in the presence of let-ins).
|
| |
|
|
| |
libraries at once (see #4193).
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
instances as definitions and lemmas do (fixes bug# 4121).
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
presence of let-ins and recursively non-uniform parameters).
The bug was in the List.chop of Inductiveops.get_arity which was wrong
in the presence of let-ins and recursively non-uniform parameters.
The bug #3491 showed up because, in addition to have let-ins, it was
wrongly detected as having recursively non-uniform parameters.
Also added some comments in declarations.mli.
|
| |
|
|
|
|
|
|
| |
number of recursively uniform parameters in the presence of let-ins.
In practice, more recursively non-uniform parameters were assumed and
this was used especially for checking positivity of nested types,
leading to refusing more nested types than necessary (see Inductive.v).
|
| | |
|
| |
|
|
| |
presence of let-ins. This fixes #3491.
|
| |
|
|
|
|
|
|
|
|
| |
Parameters were missing in the context, apparently without negative
effects because the context was used only for whd normalization of
types, while reduction (in closure.ml) was resistant to unbound rels.
See however next commit for an indirect effect on the wrong
computation of non recursively uniform parameters producing an anomaly
when computing _rect schemas.
|
| | |
|
| |
|
|
| |
+ adjusting for the removal of `admit` by Arnaud Spiwack.
|
| |
|
|
|
| |
Admitted was not using the partial proof to infer discharged variables.
Now it does. The fix makes no sense, but restore the old behavior.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- no more inconsistent Axiom in the Prelude
- STM can now process Admitted proofs asynchronously
- the quick chain can stock "Admitted" jobs in .vio files
- the vio2vo step checks the jobs but does not stock the result
in the opaque tables (they have no slot)
- Admitted emits a warning if the proof is complete
- Admitted uses the (partial) proof term to infer section variables
used (if not given with Proof using), like for Qed
- test-suite: extra line Require TestSuite.admit to each file making
use of admit
- test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to
find TestSuite.admit
|
| |
|
|
| |
universe-polymorphism mode.
|
| | |
|
| | |
|
Matthieu Sozeau
Maxime Dénès
Hugo Herbelin
Enrico Tassi
Pierre-Marie Pédrot
Pierre Letouzey
Arnaud Spiwack
Matthieu Sozeau
Jason Gross
Guillaume Melquiond