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