index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
/
g_vernac.ml4
Commit message (
Expand
)
Author
Age
*
Ajout du vernac Proof with
gregoire
2002-12-12
*
Ajout options -v7 et -v8, et commandes V7only et V8only
herbelin
2002-12-10
*
Modification Require From
mohring
2002-12-04
*
Réaffichage des Syntactic Definition (printer constr_expr).
herbelin
2002-11-26
*
Retablissement Syntactic Definition
herbelin
2002-11-25
*
Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...
herbelin
2002-11-24
*
Passage à une représentation des fixpoints plus primitive dans constr_expr ...
herbelin
2002-11-15
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
fix forbidden currified constructors
ddr
2002-11-07
*
Intégration des modifs de la branche mowgli :
herbelin
2002-11-05
*
Clarification changements autour de Remark/Fact/Local
herbelin
2002-10-23
*
Notation 2:Check et 2:Eval
herbelin
2002-10-12
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
Pb de factorisation camlp4
herbelin
2002-07-15
*
Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pour
herbelin
2002-07-11
*
Intgration uniforme de coercions dans les dclarations (Variable and co) et re...
herbelin
2002-06-03
*
Finalement un seul constr pour l'instant dans ExtraRedExpr
herbelin
2002-05-30
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
Meilleure gestion de la reduction dans Field
delahaye
2002-03-17
*
Plusieurs arguments autorisés pour Require et Read Module
herbelin
2002-01-18
*
Ajout syntaxe 'Canonical Structure' en remplacement de @Definition + suppress...
herbelin
2001-12-16
*
- condition de garde (suite)
barras
2001-12-10
*
Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR
delahaye
2001-10-23
*
Abstraction de l'immplementation de dirpath et implementation dans l'autre se...
herbelin
2001-10-17
*
Suppression option immediate_discharge; nettoyage de Declare et conséquences
herbelin
2001-10-11
*
Transparent
barras
2001-09-20
*
Parsing
herbelin
2001-08-10
*
reparation regles pour parsing Coercion Local
mohring
2001-07-13
*
Fix de quelques bugs syntaxiques de Ltac
delahaye
2001-06-11
*
Uniformisation des 'Save def_tok id'
herbelin
2001-04-09
*
nettoyage d'entrees de grammaires inutiles
courant
2001-04-09
*
mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4
filliatr
2001-04-05
*
renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...
filliatr
2001-04-04
*
entetes
filliatr
2001-03-15
*
Prise en compte noms longs dans Implicits
herbelin
2001-02-16
*
Bug point final dans la syntaxe theorem_body
herbelin
2001-02-09
*
Correction pour Time pour ne pas etre oblige de mettre deux points
delahaye
2001-02-05
*
Factorisation du '.' final
herbelin
2001-01-27
*
Prise en compte des noms longs dans les Hints et les Coercions
herbelin
2001-01-24
*
Ajout de constantes locales dans les Records
herbelin
2001-01-24
*
Ajout du Let pour le langage de tactiques
delahaye
2000-12-29
*
ajout ident_or_constrarg pour NewInduction
herbelin
2000-12-20
*
Begin-End Silent deviennent Set?Unset Silent
mohring
2000-11-21
*
Prise en compte des noms qualifiés dans certaines commandes
herbelin
2000-11-20
*
Déplacement d'une partie de g_vernac.ml4 dans g_proofs.ml4 car fichier deven...
herbelin
2000-11-05
*
compilation des fichiers ml4 sans GNUseries
filliatr
2000-11-03
*
Priorite du Try/Orelse + Debug switch + correction bug dans Pattern
delahaye
2000-10-30
*
Pattern matching de sous-termes + exceptions dans le lexer
delahaye
2000-08-17
*
Ajout syntaxe [ phr1 ... phrn ]. pour grouper des commandes (pour Time ou Gra...
herbelin
2000-07-26
*
':>' est devenu un seul token
herbelin
2000-06-02
[next]