index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
/
romega
Commit message (
Expand
)
Author
Age
*
Restructuration et simplification des fonctions d'affichage, de détypage
herbelin
2006-01-11
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...
herbelin
2005-12-26
*
Traduction des noms v7 de Z en noms v8
herbelin
2005-12-25
*
Nettoyage suite à la détection par défaut des variables inutilisées par o...
herbelin
2005-11-08
*
Pas de dépendance en Omega
herbelin
2005-02-21
*
Correction de bugs: coq_false et coq_true au lieu de coq_False et coq_true
herbelin
2005-02-21
*
- changement ordre arguments interp_goal_concl pour permettre application
herbelin
2005-02-21
*
- Correction de bugs
herbelin
2005-02-21
*
Standardisation of function names about global references (especially, renami...
herbelin
2005-02-18
*
Utilisation d'entiers en précision arbitraire pour le noyau d'omega (cf #898)
herbelin
2004-12-27
*
Remplacement du coeur d'omega (omega.ml) par la version plus gnrale utilise p...
herbelin
2004-12-27
*
Nouvelle en-tête
herbelin
2004-07-16
*
Reparation ROmega V8/Omega ZERO/POS/NEG
mohring
2004-03-04
*
adaptation V8 version Pierre Cregut
mohring
2004-03-03
*
Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...
herbelin
2003-11-29
*
Renommage canonique d'un lemme redondant
herbelin
2003-11-05
*
Renommage canonique d'un lemme redondant
herbelin
2003-11-05
*
Cacher les .v8
herbelin
2003-10-03
*
Un peu plus de souplesse dans la globalisation des noms utilises par les tact...
herbelin
2003-09-26
*
Branchement constant sur Coqlib
herbelin
2003-09-12
*
*** empty log message ***
barras
2003-03-12
*
MAJ
herbelin
2003-01-22
*
Simplification de Simplify (plus de ())
herbelin
2003-01-19
*
Problèmes et améliorations divers affichage
herbelin
2002-12-09
*
Remplacement de Syntactic Definition par Notation
herbelin
2002-11-24
*
Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...
herbelin
2002-10-13
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
ZArith_base, Zbool, Bool_nat
filliatr
2002-06-20
*
Protection des tactiques contre l'utilisation sans le bon contexte de thories
herbelin
2002-06-03
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.v
herbelin
2002-05-29
*
Prise en compte des corps de letin dans les hypothèses
herbelin
2002-03-01
*
convert_hyp a change de type
barras
2002-03-01
*
compat ocaml 3.03
filliatr
2001-12-13
*
GROS COMMIT:
barras
2001-11-05
*
Abstraction de l'immplementation de dirpath et implementation dans l'autre se...
herbelin
2001-10-17
*
Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...
herbelin
2001-10-12
*
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-10-09
*
Romega
mohring
2001-09-20
*
MAJ V7.1
herbelin
2001-09-19
*
reparation Zne
mohring
2001-09-19
*
Romega/names/Makefile
mohring
2001-09-18