index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
command.ml
Commit message (
Expand
)
Author
Age
*
Si un fixpoint a plusieurs arguments, mais un seul de type inductif,
letouzey
2006-04-14
*
Finalement, scopes utiles pour option 'where' (cf bug #1132)
herbelin
2006-04-07
*
Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.
msozeau
2006-03-13
*
Correction du bug 808: il est maintenant interdit de déclarer une assomption...
coq
2006-03-02
*
Bug correction in saving proofs: If a hook opens a proof but does not close i...
bertot
2006-02-13
*
warning seulement si mode verbose
herbelin
2006-02-06
*
Réorganisation de la structure interne des types de déclarations (decl_kinds)
herbelin
2006-01-28
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-26
*
Restructuration des points d'entrée de Pretyping et Constrintern
herbelin
2005-12-21
*
Orthographe de 'instantiate'
herbelin
2005-12-17
*
Changement des named_context
gregoire
2005-12-02
*
Nettoyage suite à la détection par défaut des variables inutilisées par o...
herbelin
2005-11-08
*
Types inductifs parametriques
mohring
2005-11-02
*
Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...
herbelin
2005-01-02
*
Rétablissement d'un vrai Eval sous le contexte des définitions, pas un qui ...
herbelin
2004-12-30
*
Bug (cf #892)
herbelin
2004-12-06
*
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
sacerdot
2004-11-16
*
Changement dans les boxed values .
gregoire
2004-11-12
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
Suppression IsConjecture redondant avec Conjectural
herbelin
2004-10-11
*
hiding the meta_map in evar_defs
barras
2004-09-15
*
Nouvelle en-tête
herbelin
2004-07-16
*
correspondance des records et noms de champs de records entre un module et sa...
letouzey
2004-06-25
*
Export de l'information si un inductive est un record ou non (pour xml)
herbelin
2004-03-31
*
Distinction entre declarations internes (p.ex. _subproof) et declarations uti...
herbelin
2004-03-30
*
Gestion maintenant purement fonctionnelle des implicites des point-fixes; ajo...
herbelin
2004-03-27
*
modif des fixpoints pour que si on donne une notation au produit, les pts fix...
barras
2004-03-05
*
Keep structure information for Fixpoint declaration and Fix terms
bertot
2004-02-26
*
Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :...
herbelin
2004-01-29
*
Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables a...
herbelin
2004-01-13
*
meilleure presentation des commentaires du traducteur
barras
2004-01-02
*
Conjecture declare maintenant un axiome; reorganisation VernacDefinition
herbelin
2003-10-23
*
Changement 'as notation' en 'where notation'; Plus d'uniformite dans la gesti...
herbelin
2003-10-14
*
Admitted rendu independant de Conjecture: plus pratique en mode interactif
herbelin
2003-10-13
*
Bug introduit dans start_proof par le commit precedent
herbelin
2003-10-13
*
Protection contre les noms de lemmes existant deja
herbelin
2003-10-13
*
Prise en compte des paramètres implicites d'inductifs pour la globalisation ...
herbelin
2003-10-08
*
Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...
herbelin
2003-10-08
*
(Re-)branchement sur les noms reserves pour les args d'inductif (dont Record)...
herbelin
2003-09-16
*
Déplacement de Declare et déclarations des scopes d'argument dans Declare
herbelin
2003-09-12
*
Mise en place possibilité de définitions locales dans les paramètres des i...
herbelin
2003-09-06
*
Mise en oeuvre de la syntaxe des inductifs a la ML 'Inductive nat : Set := O ...
herbelin
2003-08-31
*
Mise en place structure pour des 'arguments scope' dirigés par une classe
herbelin
2003-06-10
*
Possibilité de syntaxe conjointement à la définition des inductifs et des ...
herbelin
2003-05-21
*
Prise en compte des syntaxes v8 dans Uninterpreted Notation
herbelin
2003-04-29
*
Ajout "at next level" dans Notation
herbelin
2003-04-17
*
Ajout option 'Local' à Infix et Notation
herbelin
2003-04-11
*
Réorganisation de Impargs + mise en place d'une infrastructure
herbelin
2003-04-09
*
Ajout d'un choix 'onlyparse'
herbelin
2003-03-31
*
Implicit Variables Type dans les inductive
herbelin
2003-03-29
[next]