index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
.depend.camlp4
Age
Commit message (
Expand
)
Author
2005-03-16
tactiques prouveurs premier ordre dans contrib/dp/
coq
2005-02-04
Ajout g_xml.ml4 et cic2Xml.ml
herbelin
2004-08-26
maj
filliatr
2004-07-29
maj
filliatr
2004-07-16
MAJ
herbelin
2004-05-04
maj
filliatr
2004-01-28
maj
filliatr
2004-01-15
maj
filliatr
2003-10-16
Ground update + Linear removal
corbinea
2003-07-02
suppression de newtauto
corbinea
2003-06-15
Ground major update ... mmm, sounds exciting !
corbinea
2003-05-26
moved engine.ml4 to ground.ml4, added option 'Ground Depth'
corbinea
2003-04-25
Added the Ground tactic.
corbinea
2003-03-12
* Ajout du traducteur nouvelle syntaxe *
barras
2003-02-28
maj
filliatr
2003-02-27
The contribution of Pierre Courtieu on generating specialized induction schemes
bertot
2003-02-24
Bringing Linear back to life (Still somewhat buggy).
corbinea
2003-01-23
Ajout de LinearIntuition; Ajout de New(Tauto|Intuition|LinearIntuition).
corbinea
2002-11-14
Réforme de l'interprétation des termes :
herbelin
2002-11-05
Intégration des modifs de la branche mowgli :
herbelin
2002-10-01
Adding the congruence closure tactics (CC and CCsolve).
corbinea
2002-09-20
maj
filliatr
2002-09-20
maj
filliatr
2002-08-02
Modules dans COQ\!\!\!\!
coq
2002-06-07
extraction vers scheme
letouzey
2002-05-29
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2001-12-19
contrib/interface/dad.ml4 had no real need of streams, it should have been
bertot
2001-12-19
reparation du make depend et du .depend
letouzey
2001-06-25
Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...
herbelin
2001-06-25
Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...
herbelin
2001-04-19
Ajout de Field
delahaye
2001-04-10
réparation Correctness; options Extraction (changement de syntaxe)
filliatr
2001-04-08
Ajout lemmes arithmetiques
mohring
2001-03-30
branchement extraction (bytecode seulement)
filliatr
2001-02-08
simplification du make depend; fonctions de stat. util. memoire dans certains...
filliatr
2001-02-05
calcul des dependances camlp4 et production directe ml4 -> cmo (avec Judicael)
filliatr
2000-11-29
mise a jour
filliatr
2000-11-05
MAJ
herbelin
2000-11-03
compilation des fichiers ml4 sans GNUseries
filliatr
2000-10-31
- simplification Makefile (compilation des fichiers .ml'; pas encore parfait
filliatr
2000-09-18
mise a jour dependances
filliatr
2000-09-10
Suppression de Abst
herbelin
2000-03-08
MAJ
herbelin
2000-01-07
Renommage command en constr
herbelin
1999-12-05
premier debugage
filliatr
1999-12-03
- global_reference traite des variables
filliatr
1999-10-20
modules Evar_refiner et Typing_ev
filliatr