| Commit message (Collapse) | Author | Age |
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10077 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
modification de interp_ltac_reference pour passer les ids utilisées
dans le contexte d'appel d'une tactique.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10076 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10075 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
un commentaire)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10074 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10073 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
implicitement suggéré par le rapport de bug #1671
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10072 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
rapport de bug #1671 - mais ne résoud pas le #1671 dans le propos peut
être vu comme le souhait de voir traité le cas simple du problème
généralement indécidable d'inversion des contraintes des types
inductifs)
- Petite amélioration dans le nommage des variables dans expand_arg
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10070 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10069 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
bugs soumis sur Coq-bugs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10068 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
iter_constr_with_full_binders + documentation de Guarded.
--Cette ligne, et les suivantes ci-dessous, seront ignorées--
M trunk/doc/refman/RefMan-pro.tex
M trunk/pretyping/inductiveops.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10065 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10064 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10063 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10062 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10061 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
purpose and can be used directly be the user. Document them. Change Prelude to disambiguate an import of a Tactics module.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10060 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
equalities. Useful to do so-called "ford" induction.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10059 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10058 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
- BSD compatibility: do not use -printf action of find (2nd round)
- don't recurse into VCS metadata for file lists
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10057 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10056 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10055 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
stdlib/index-body.html.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10051 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
recommended way more explicitly.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10050 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
standard:
- ajout d'une entrée dans le Makefile principal pour le fichier de
globalisations glob.dump
- modifications de doc/Makefile et de l'index html pour gérer les
nouveaux fichiers de la librairie standard (en part. ceux dans
Ints)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10049 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
do_norm. Corrigé par analogie avec N11, N12, ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10048 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10046 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10045 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10043 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
Cleaner code: the guardedness bug is now corrected.
Added "trivial" to the automation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10042 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10041 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10040 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
to bad cache handling.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10032 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10029 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
------------------------------------------------
See file PreOmega for more details and/or test-suite/succes/*Omega*.v
The zify tactic performs a Z-ification of your current goal,
transforming parts of type nat, N, positive, taking advantage of many
equivalences of operations, and of the positivity implied by these
types.
Integration with omega and romega:
(r)omega : the earlier tactics, 100% compatible
(r)omega with * : full zify applied before the (r)omega run
(r)omega with <types>, where <types> is a sub-list of {nat,N,positive,Z},
applies only specific parts of zify (btw "with Z" means take advantage
of Zmax, Zmin, Zabs and Zsgn).
As a particular consequence, "romega with nat" should now be a
close-to-perfect replacement for omega. Slightly more powerful, since
(forall x:nat, x*x>=0) is provable and also slightly less powerful: if
False is somewhere in the hypothesis, it doesn't use it.
For the moment zify is done in a direct way in Ltac, using rewrite
when necessary, but crucial chains of rewrite may be made reflexive
some day.
Even though zify is designed to help (r)omega, I think it might be
of interest for other tactics (micromega ?). Feel free to complete
zify if your favorite operation / type isn't handled yet.
Side-effects:
- additional results for ZArith, NArith, etc...
- definition of Ple, Plt, Pgt, Pge and notations for them in positive_scope
- romega now start by doing "intros". Since the conclusion will be negated,
and this operation will be justified by means of decidability, it helps
to have as little as possible in the conclusion.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10028 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10027 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
complains.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10026 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10025 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10024 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10023 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10022 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
frais (par exemple pour "intro") ou pas forcément (par exemple pour
"fresh")
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10021 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10020 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
noté cette erreur de ma part (copier/coller mon amour).
Ça créait des soucis dans les dépendance dans l'ancienne architecture de
Makefile, probablement dans la nouvelle aussi dans certaines
circonstances. Exit les bêtise, c'est plus propre maintenant.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10019 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
- Make sure make notices when a command fails
- don't leave behind half-baked output files of commands that failed
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10016 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
anymore.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10015 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10013 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10012 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The -MG option causes gcc to add any non-found .h file verbatim in the
dependencies. This naturally doesn't include the path to it (because
the path is unknown) and thus make doesn't know how to build it; it
knows how to build kernel/byterun/coq_jumptbl.h, not "coq_jumptbl.h".
--This line, and those below, will be ignored--
M Makefile.common
M Makefile.build
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10011 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10010 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10009 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10008 85f007b7-540e-0410-9357-904b9bb8a0f7
|