index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
Commit message (
Expand
)
Author
Age
*
Messages de idtac et fail peuvent maintenant être des listes de string, int ...
herbelin
2006-01-21
*
Ajout de la contrainte que l'assertion doit être complètement prouvée dans...
herbelin
2006-01-21
*
Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et f...
herbelin
2006-01-21
*
Déplacement de pr_arg et pr_opt de Ppconstr vers Util
herbelin
2006-01-21
*
Retrait de 'by' comme mot-clé en espérant qu'il n'y aura pas d'interférenc...
herbelin
2006-01-18
*
Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq
herbelin
2006-01-16
*
- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses
herbelin
2006-01-16
*
cvs ci -m "Passage à la limite dans les intro-pattern de n-uplets"
herbelin
2006-01-16
*
Ajout de nouvelles plages de symboles unicode; prise en compte des indices un...
herbelin
2006-01-15
*
Bug (code prévu pour iso-latin et non utf-8)
herbelin
2006-01-15
*
Code mort du traducteur
herbelin
2006-01-14
*
Compatibilité prterm
herbelin
2006-01-12
*
Suite réorganisation des fonctions d'affichage
herbelin
2006-01-11
*
Restructuration et simplification des fonctions d'affichage, de détypage
herbelin
2006-01-11
*
Suppression redondance coerce_to_id dans Pcoq et constrintern et déplacement...
herbelin
2006-01-09
*
Automatisation de l'utilisation de token primitifs dans les motifs de filtrage
herbelin
2006-01-08
*
Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux de...
herbelin
2005-12-30
*
Mini-restructuration
herbelin
2005-12-30
*
Commentaire mort
herbelin
2005-12-28
*
Remplacement Pp.qs par Pptactic.qsnew
herbelin
2005-12-28
*
Autres suppressions de composantes du traducteur
herbelin
2005-12-27
*
Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...
herbelin
2005-12-26
*
Petite correction nom QuantHypArgType suite suppression traducteur
herbelin
2005-12-26
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-26
*
Simplifification de vernac_expr li l'abandon du traducteur
herbelin
2005-12-23
*
Correction printer des Tactic Notation
herbelin
2005-12-23
*
Restructuration des points d'entrée de Pretyping et Constrintern
herbelin
2005-12-21
*
Ajout printer pr_lconstr aux extensions de syntaxe pour les arguments de tact...
herbelin
2005-12-21
*
Changement des named_context
gregoire
2005-12-02
*
Correction bug dé-globalisation syntactic def (cf coq-club 20/11/05)
herbelin
2005-11-21
*
*** empty log message ***
barras
2005-11-18
*
Nettoyage suite à la détection par défaut des variables inutilisées par o...
herbelin
2005-11-08
*
- debugging og "Show Intros": no line breaking + fresh ids
coq
2005-11-08
*
Types inductifs parametriques
mohring
2005-11-02
*
Niveau 99 permettant de parser { } nécessaire aussi dans l'entrée pattern
herbelin
2005-09-21
*
pas besoin de List.length pour savoir si une liste est vide
letouzey
2005-08-19
*
Add some debug printing functions.
coq
2005-07-15
*
Added entry constr_may_eval for tactic extensions (new syntax)
herbelin
2005-06-22
*
Ajout explicite du niveau 200 de pattern auquel on fait référence au niveau...
herbelin
2005-06-04
*
New command: "Print Ltac qualid" to print user defined tactics.
sacerdot
2005-05-20
*
Adoption du nom canonique global_of_constr pour éviter confusion avec type r...
herbelin
2005-05-20
*
Affinements suite à extension Tactic Notation aux tacticielles
herbelin
2005-05-17
*
Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...
herbelin
2005-05-17
*
Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...
herbelin
2005-05-17
*
Globalisation des Tactic Notation
herbelin
2005-05-15
*
Allow auto to have a parametric argument (wish #967)
herbelin
2005-05-15
*
possibilité d'écrire [foo| ] au lieu de [foo|idtac]
letouzey
2005-05-09
*
Code v7 obsolete
herbelin
2005-05-05
*
Implementation of a new backtracking system, that allow to go back
coq
2005-04-20
*
Added 'clear - id' to clear all hypotheses except the ones dependent in the s...
herbelin
2005-03-07
[next]