| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
| |
error messages. The architecture of unification error handling
changed, not helped by ocaml for checking that every exceptions is
correctly caught. Report or fix if you find a regression.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16205 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
interleaving of ltac and ml code is not visible (this particularly
applies to ltac notation ring, which calls ml-level ring_lookup and
Ring again at the ltac level, resulting in non-localisation of "ring"
errors).
Added also missing LtacLocated checks in Class_instance and Proofview.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16204 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
variable names).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16185 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16181 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
the presence of aliased modules). Bug was actually fixed in trunk
(thanks to PMP's monomorphization (and change of semantics) of
equality over evaluable references.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16180 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
to inconsistency in using evar_hyps which is unfiltered and evar_env
which is filtered).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16175 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16168 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
the function solve_candidates introduced in 8.4).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16163 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16133 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16132 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16129 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
(e.g. 1 for eq_refl).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16094 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
an evar in typing.ml. Thanks to HoTT people for noticing the problem.
Fixed behavior of e_typing
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16092 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
different instances of a meta are checked against full conversion.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16086 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
IT happens that there are some other uses of casts, e.g. in nat_int de
MathClasses which uses a notation 0 for some class constructor zero,
and a cast (0:nat) to force this notation 0 to represent the instance
O in nat of the class of types having a zero (eventually, 0,
i.e. "zero nat O" and "O" are convertible but the information of being
a class instance is lost).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16024 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
notations: - hopefully never 2 spaces when the user did not ask for -
more systematic default insertion of spaces around symbols - e.g. have
space before "[" if after a non-terminal - have spaces between
consecutive terminals
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16019 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16011 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
check condition in pattern-unification, resulting in the instantiation
of evars by terms depending on themselves, henceforth leading
eventually to a stack overflow. Occur-check in the arguments of evars
was also missing.
[Also fixed what looked like a typo in the env passed to
project_evar_on_evar on line 1611.]
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15996 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15990 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
universes. As it uses eq_rect on Type(2), the arguments of eq_rect
has to be in Type(3) and compiling the standard library now needs one
more universe! If needed, we could avoid this by inlining the
definition of (eq_rect Type2) in Hurkens.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15981 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15980 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
type in "cast" to activate the temporary interpretation scope.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15978 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15906 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15770 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15769 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15767 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15757 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
We now always produce two binaries, coqtop and coqtop.byte :
- If ocamlopt is available, coqtop is directly what used to be coqtop.opt,
no more symlinks needed.
- Otherwise, coqtop is a copy of coqtop.byte.
The same for coqchk and coqide...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15752 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
It uses a term in front of a stack instead of a term in front of a list of applied
terms. From outside of eq_appr_x nothing should have changed.
Nasty evar instantiation bug
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15719 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
current evar to project; this may happen if this evar is dependent and
is involved in evar-evar conversion problem eventually solved by
instantiating the current evar; could maybe be optimized when the evar
to materialize has invertible instance in which case
define_evar_from_virtual_equation applied on the current evar could be
shortcut, avoiding to create an evar).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15657 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
standard under lambdas and products).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15644 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
variable is used both as term and as binder, resulting in
ununderstandable error message about scopes).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15642 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15585 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
situations (see rewrite MonoidMonadTrans.bind_toLower' in
Misc/QuicksortComplexity/monoid_expec.v).
Also fixing badly designed test 2817.v.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15543 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15542 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
One slight point to check someday : fourier used to
launch a tactic called Ring.polynom in some cases.
It it crucial ? If so, how to replace with the setoid_ring
equivalent ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15524 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Most of these heavyweight annotations were introduced a long time ago
by the automatic 7.x -> 8.0 translator
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15517 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- For instance, refl_equal --> eq_refl
- Npos, Zpos, Zneg now admit more uniform qualified aliases
N.pos, Z.pos, Z.neg.
- A new module BinInt.Pos2Z with results about injections from
positive to Z
- A result about Z.pow pushed in the generic layer
- Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l}
- Using tactic Z.le_elim instead of Zle_lt_or_eq
- Some cleanup in ring, field, micromega
(use of "Equivalence", "Proper" ...)
- Some adaptions in QArith (for instance changed Qpower.Qpower_decomp)
- In ZMake and ZMake, functor parameters are now named NN and ZZ
instead of N and Z for avoiding confusions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
known instances in unification.ml). This refines the fix to bug #1918.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15459 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
bad interaction between lazy evaluation of pp streams and temporary
effectful extension of global environment).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15457 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
It used to be the case that the list of declared section variables
for a constant was taken into account only when discharging the first
enclosing sections, but not any outer section. Example of the bug:
Section A. Variable x : bool.
Section B. Variable y : nat.
Lemma foo : True. Proof using x y. Admitted.
End B. End A.
Check foo. (* nat -> True instead of bool -> nat -> True *)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15445 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15440 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15433 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15431 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Fixes the test-suite.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15324 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
There is a warning if the term is more precise.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15252 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15241 85f007b7-540e-0410-9357-904b9bb8a0f7
|