index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
command.mli
Commit message (
Expand
)
Author
Age
*
Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...
herbelin
2003-10-08
*
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
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Intégration des modifs de la branche mowgli :
herbelin
2002-11-05
*
Clarification changements autour de Remark/Fact/Local
herbelin
2002-10-23
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
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
*
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
*
Suite de la suppression : enamed_declaration est remplace par evar_map.
clrenard
2001-11-06
*
GROS COMMIT:
barras
2001-11-05
*
Suppression option immediate_discharge; nettoyage de Declare et conséquences
herbelin
2001-10-11
*
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-10-09
*
Parsing
herbelin
2001-08-10
*
Uniformisation des 'Save def_tok id'
herbelin
2001-04-09
*
entetes
filliatr
2001-03-15
*
Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...
herbelin
2001-01-24
*
Réorganisation suite ajout de constantes locales dans les Records
herbelin
2001-01-24
*
Ajout du Let pour le langage de tactiques
delahaye
2000-12-29
*
Découpage des différentes fonctionnalités de build_mutual et definition_st...
herbelin
2000-12-19
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
Distinction local/global
herbelin
2000-11-27
*
Renommage canonique :
herbelin
2000-10-18
*
Déplacement de save_thm and co de PFedit vers Command
herbelin
2000-05-25
*
export get_current_context
herbelin
2000-05-18
*
Nettoyage de l'interface de Pfedit
herbelin
2000-05-04
*
Nettoyage des fichiers de parsing
herbelin
2000-01-13
*
Les inductifs dans Scheme doivent être des ident d'inductifs
herbelin
1999-12-15
*
documentation interfaces
filliatr
1999-12-13
*
modifs pour premiere edition de liens
filliatr
1999-12-02
*
module Command
filliatr
1999-12-02
*
module Metasyntax
filliatr
1999-12-01