| Commit message (Collapse) | Author | Age |
... | |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
un problème dû à la non réversibilité de la suppression de règles
camlp4 vis à vis de l'insertion : lorsqu'un niveau existant vide est
étendu, la suppression non seulement efface l'extension mais aussi le
niveau lui-même. Ceci a un effet sur les niveaux vides 8 et 99. Nous
n'avons pas trouvé de bonne solution à ce problème et l'utilisation
d'extensions aux niveaux 99 ou 8 (anciennement 5 avant ce commit)
continue de corrompre le parser si effectuées à l'intérieur de section
ou de modules. Voici un exemple montrant le problème :
Print Grammar constr. (* le niveau "8" existe *)
Section A.
Notation "{{ x }}" := (S x) (at level 8).
End A.
Print Grammar constr. (* le niveau "8" n'existe plus *)
Goal True.
apply I. (* appelle le niveau constr qui continue d'appeler "8"... échec *)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9756 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
tout en évitant que les .. soient dans constr)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9755 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9333 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9043 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
pattern pose problème pour les notations ajoutées à ce niveau; qu'à cela ne tienne, l'associativité du niveau 100 pour pattern n'est pas importante : on le rend RIGHTA
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9008 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8996 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
'ExtraArgType "tacticX"' (0<=X<=5) créé dynamiquement, ceci afin de
pouvoir typer correctement les wit_tactic (auparavant le typage des
wit_tactic était trop libéral et permettait de casser la
subject-reduction).
Amélioration au passage de l'affichage de la tactique "replace by"
(module Extratactics).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8926 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
déplacement dans Topconstr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7826 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7761 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
(mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7732 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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7162 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
aux niveaux syntaxiques des tacticielles
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7029 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
"T with (Definition|Module) M1.M2....Mn.id := c" (in the ML style).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6582 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
n'est pas assez puissante pour retarder la coercion vers le but au dernier moment
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6458 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6426 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
tactiques d'appliquer une éventuelle coercion vers le but
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6408 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6259 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
au passage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5510 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
noms d'hypothèses
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5419 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
des IntroPattern au parsing, à l'interprétation, à la traduction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5405 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5355 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
par un niveau ajoute dynamiquement
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5068 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Changement des exports pour tactic EXTEND : with_bindings devient bindings qui prend plus le with, il faut le mettre à la main dans la règle.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5052 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5002 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
operconstr et pattern: plus de niveaux vides
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4956 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
par le delete_rule de camlp4
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4947 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4929 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4832 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
extensions de la grammaire des motifs de Cases
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4758 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
associative a gauche; gestion du signe dans le parseur pas dans l'interpreteur
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4745 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Hint Destruct: syntaxe similaire aux autres hints...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4696 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4670 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4559 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4554 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4432 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4268 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Option -v8 à coqtop lance coqtopnew
Le terminateur reste "." en v8
Ajout construction primitive CLetTuple/RLetTuple
Introduction typage dans le traducteur pour traduire les Case/Cases/Match
Ajout mutables dans RCases or ROrderedCase pour permettre la traduction
Ajout option -no-strict pour traduire les "Set Implicits" en implicites stricts
+ Bugs ou améliorations diverses
Raffinement affichage projections de Record/Structure.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4257 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Mise en place structure pour définir un objet en même temps que sa notation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3939 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3794 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
Nouvelle entrée "annot" pour contourner le conflit entre ">" et les
annotations entre piquants
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3440 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
quand mentionn explicitement par l'utilisateur
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3377 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3348 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3343 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3332 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3314 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
Affinement de la gestion des niveaux de constr.
Cablage en dur du parsing et de l'affichage des délimiteurs de scopes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3295 85f007b7-540e-0410-9357-904b9bb8a0f7
|