| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
| |
unsatisfiable constraints.
Add a resolution call in tacinterp before trying the default tactic.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11131 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
disambiguate syntax:
[ H := [ ?x ] : context C [ foo ] |- _ ] is ok, as well as [ H := ?x :
nat |- _ ] or [H := foo |- _ ], but [ H := ?x : context C [ foo ] ] will
not parse.
Add applicative contexts in tactics match, to be able to match arbitrary partial
applications, e.g.: match f 0 1 2 with appcontext C [ f ?x ] => ... end
will bind C to [ ∙ 1 2 ] and x to 0.
Minor improvements in coqdoc.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11129 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
restriction du contexte était attendue) + suppression warning +
amélioration affichage en cas de clause "at" incorrecte + report
commit 11121 (correction bug 1367) de la 8.2 vers le trunk.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11128 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
- dans le "replay", l'état n'était pas correctement sauvegardé d'où une
perte d'efficacité en cas de rejeux répétés,
- bug de synchronisation dans le calcul de la pile des lemmes ouverts.
+ réajout de la variante standard de Set Printing All dans le menu display.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11125 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
globals. Change program_simpl to use [auto] and not [auto with *].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11124 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11123 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
latex, qui empechait de produire des fichiers .dvi à partir des .tex
générés par coqdoc.
--Cette ligne, et les suivantes ci-dessous, seront ignorées--
M trunk/tools/coqdoc/coqdoc.sty
M branches/v8.2/tools/coqdoc/coqdoc.sty
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11120 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
in order for them to preserve the structural order.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11115 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11114 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11113 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11112 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
dans la recherche du nom long était bien utile (parce que la table des
filename n'est plus synchronisée et plus dans le initial.coq) mais
c'est ailleurs qu'on reposait à tort sur la bonne synchronisation de
la table des noms longs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11111 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
des filename hors reset (r11077).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11110 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11107 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11106 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
components and resolving them separately, reporting more precise failures.
Improve error messages.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11105 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11103 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11102 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
buts, on se base sur les informations de Pfedit (comme le fait Pierre
Courtieu). Permet d'être plus robuste sur les extensions de syntaxe
ouvrant des buts, style Function.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11101 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11100 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11099 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11098 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11097 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
- Test match dépendant.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11095 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Changement au passage de la convention "at -n1 ... -n2" en
"at - n1 ... n2" qui me paraît plus clair à partir du moment où on peut
pas mélanger des positifs et des négatifs.
- Au passage:
- simplification de gclause avec fusion de onconcl et concl_occs,
- généralisation de l'utilisation de la désignation des occurrences par la
négative aux cas de setoid_rewrite, clrewrite et rewrite at,
- correction d'un bug de "rewrite in at" qui utilisait le at de la
conclusion dans les hyps.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11094 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11093 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
letting the exception go uncatched.
- Reorder definitions in Morphisms, move the PER on (R ==> R') in
Morphisms where it can be declared properly. Add an instance for
Equivalence => Per.
- Change bug#1604 test file to the new semantics of [setoid_rewrite at]
- More unicode characters parsed by coqdoc.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11092 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11091 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
fait remarquer Bruno, c'est ne pas anodin de laisser croire qu'on
admet une conjecture alors qu'on admet uniquement la conclusion de
cette conjecture, conclusion qui peut être incohérente et qui ne le
serait pas si on avait gardé le contexte du but.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11089 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11088 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* In order to get via a "SearchAbout bigZ" all the generic lemmas that are
now available, I moved bigZ to a notation for BigZ.t instead of a definition.
But this notation was interacting badly with the number parsing.
* Moreover, I also discovered that printing was broken as well, due to a
reference to obsolete name Basic_type (now DoubleType) that I forgot to
adapt in g_intsyntax.
* Last but not least, there was also a bug not due to myself that was probably
preventing parsing/printing _very_ big numbers (the ones for which generic
constructor BigN.Nn is used): this Nn is the 7-th constructor, not the 13-th.
In addition, the first argument to Nn was supposed to be automatically inferred,
this was not working, so we build it now explicitely (very easy).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11087 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
le bug #1867
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11086 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
- Correction wish 1866 (un "admit" plus fin dans sa généralisation des hyps)
- Bricoles dans cases.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11085 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
imbriqués) du bug 1834, mais le bug 1834 reste ouvert [cases.ml].
- Réactivation de l'interprétation des listes dans "generalize" cassée
depuis 11072) [tacinterp.ml].
- Bricoles et petit nettoyage en passant [cases.ml et g_vernac.ml4].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11083 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11082 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11081 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11080 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
coq_makefile
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11079 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
de preuves imbriquées.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11078 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Relecture, mise à jour, correction d'erreurs et petite
réorganisation du chapitre sur les commandes vernaculaires.
- Correction bug #1865 (rafraichissement des univers algébriques).
- Suppression de la dépendance du initial.coq en les noms longs des fichiers
de façons à ce que les dépendances ne soient que purement logique.
- Encore un (petit) bug undo ide.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11077 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11076 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11075 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11074 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
- MAJ CHANGES et COMPATIBILITY
- Réservation de || et && dans Notations.v
- code mort et MAJ suite commit 11072 (tactics.ml et changes.txt)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11073 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Ajout clause "in" à "remember" (et passage du code en ML).
- Ajout clause "in" à "induction"/"destruct" qui, en ce cas, ajoute
aussi une égalité pour se souvenir du terme sur lequel l'induction
ou l'analyse de cas s'applique.
- Ajout "pose t as id" en standard (Matthieu: j'ai enlevé celui de
Programs qui avait la sémantique de "pose proof" tandis que le nouveau
a la même sémantique que "pose (id:=t)").
- Un peu de réorganisation, uniformisation de noms dans Arith, et
ajout EqNat dans Arith.
- Documentation tactiques et notations de tactiques.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11072 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11071 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11070 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
exception for dependent arrow types.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11069 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
matched occurences that are not selected. Permit to rewrite at 3
different places in (a + b) + (c + d) = 0 with a lemma ending in [_ +
_]. Order is depth-first and left-to-right.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11068 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11067 85f007b7-540e-0410-9357-904b9bb8a0f7
|