| Age | Commit message (Collapse) | Author |
|---|
|
user contribs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- deletion of some dead code
- grouping all stuff depending on Z in a nice module Int
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10000 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
utilities from Util. Some additions in Util, and simplifications
in various files.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9969 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
-----------------------------------
All romega tests in the test-suite are now bug-free. The only known
remaining limitation of romega with respect to omega is that it cannot
handle stuff on nat.
* Equivalences A<->B are now understood by romega (as well as omega),
and seen as (A->B)/\(B->A). There might be a smarter way to procede,
for instance having a primitive Iff construct and trying to break
equivalences as late as possible.
* Conclusion-as-Pprop issue:
After the resolution by the abstract omega machinery, useless parts
are discarded from the reification process by replacing them with
Pprop construct (see really_useful_prop). This allow to decrease
the size of the proof terms and speed up their normalisation, I guess.
But when such Pprop are created in the conclusion, this leads to
failure, since concl is negated, and this is donc only if it is
decidable. And introducing some Pprop might change the decidability
status of the concl: for instance, Pfalse is decidable, whereas
Pprop False is considered as _not_ decidable. Quick fix: no more
really_useful_prop applied on concl (needs careful computation of
useful_var).
* NEGATE_CONTRADICT(_INV):
This trace instrution comes in fact in two flavors, according to a
boolean flag. We now translate to O_NEGATE_CONTRADICT_INV if this
flag is false. (fix Besson's bug #1298)
* EXACT_DIVIDE:
could be used on NeqTerm and not only on EqTerm.
* h_step indexes:
The abstract omega machinery can introduce new hyps. In the list of hyps,
they appears _before_ the regular one (but after the goal seen as an hyp
by negating it). But the normalization steps were applied to regular hyps
thanks to their indexes counted _before_ the addition extra hyps.
* extra hyps (a)normal forms:
extra hyps and variables are initially of the shape
poly(v1,...,v(n-1)) = vn
but O_STATE was expecting them in form 0 = poly(...) + -vn
(by the way, SPLIT_INEQ should be checked someday).
Since the above is one weekend's worth of debugging, there might well
remain some more bugs :-(.
For the record, here's the less painful way to debug a failed romega run:
- activate debug flag in omega.ml and refl_omega.ml
- at the bottom of refl_omega, replace normalise_vm_in_concl with
convert_no_check (see comment there): this allow to skip the usually
_huge_ error message about "Impossible to unify True with ..."
- run the romega
- try to run Qed, and enjoy the nice errror message about a
(omega_tactic ? ? ? ?) that should be reducible to True.
Here starts the real debug work...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9962 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8660 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
1) dans refl_omega, on donnait a OmegaSolver un generateur de numero
d'equations new_eq_id qui pouvait clasher avec les numeros d'equations
initiaux créés avec new_omega_id.
=>
on sépare en deux compteurs, un pour les equations omegas, l'autre
pour les variables omegas. On en profite pour reinitialiser ces
compteurs à chaque session romega, histoire que romega devienne
reproductible.
2) dans omega.ml, le role de new_eq_id et new_var_id etait interverti
à un endroit.
ATTENTION: ceci peut changer le comportement d'omega. Surveiller le
resultat du prochain bench nocturne.
3) dans ReflOmegaCore.v, on ne traitait pas le cas d'une implication
dans une hypothese lors du recalcul final.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8657 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
et d'"externalisation"; standardisation du nom des fonctions d'affichage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(mcanismes de renommage des noms de constantes, de module, de ltac et de certaines variables lies de lemmes et de tactiques, mcanisme d'ajout d'arguments implicites, etc.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7734 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7726 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
ocaml 3.09
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- filtrage sur Bigint.zero incorrect: zero était considéré comme une variable
- coq_false et coq_true au lieu de coq_False et coq_true
- vérification chargement ROmega.vo
- Divers
- changement ordre argument interp_goal_concl pour permettre
application partielle
- amélioration débogueur
- ajout interprétation Zsucc, Zopp, et gel de Zmult si non scalaire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6761 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6514 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
par romega (omega2.ml, qui, l'occassion, disparat sous ce nom)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6511 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5431 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5428 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3394 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2745 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
commandes vernaculaires (cf dev/changements.txt pour plus de précisions)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2734 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2505 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2503 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2014 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1989 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1980 85f007b7-540e-0410-9357-904b9bb8a0f7
|
