index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Introduction de syntaxe convivial +,*,<=,<,>=
herbelin
2002-05-29
*
Double Induction prend maintenant des noms d'hyppthèses
herbelin
2002-05-29
*
Utilisation d'Infix/Distfix autant que possible
herbelin
2002-05-29
*
Contournement des My_special_variable
herbelin
2002-05-29
*
*** empty log message ***
herbelin
2002-05-29
*
Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.v
herbelin
2002-05-29
*
Fichiers tactics/*.ml4 remplacent les tactics/*.v
herbelin
2002-05-29
*
Ajout EVAL
herbelin
2002-05-29
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
Réorganisation des tclTHEN (cf dev/changements.txt)
herbelin
2002-05-29
*
Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.v
herbelin
2002-05-29
*
Fichiers tactics/*.ml4 remplacent les tactics/*.v
herbelin
2002-05-29
*
Pour les tactiques dépendant de False
herbelin
2002-05-29
*
Implante la macro camlp4 VERNAC COMMAND EXTEND
herbelin
2002-05-29
*
Implante la macro camlp4 TACTIC EXTEND
herbelin
2002-05-29
*
Fichier des expressions de commandes vernaculaires
herbelin
2002-05-29
*
Fichier des expressions de tactiques
herbelin
2002-05-29
*
MAJ 7.3
herbelin
2002-05-29
*
Ajout Hurkens.v, ProofIrrelevances.v et l'indiscernabilite dans Classical_Prop.v
herbelin
2002-05-29
*
Ajout de Eval, Inst et Check
delahaye
2002-05-27
*
Changement Filename.is_relative en Filename.is_implicit, plus pertinent
herbelin
2002-05-27
*
Oublis
herbelin
2002-05-22
*
*** empty log message ***
desmettr
2002-05-22
*
*** empty log message ***
herbelin
2002-05-22
*
Correction of a bug in Intuition (no more decomposition of dependent pairs).
corbinea
2002-05-22
*
Field + MapleMode
delahaye
2002-05-21
*
MAJ
herbelin
2002-05-16
*
ARCH passe de Makefile à config.distrib
herbelin
2002-05-16
*
MAJ
herbelin
2002-05-16
*
MAJ V7.3
herbelin
2002-05-16
*
Ajout Peano_dec et Compare_dec
herbelin
2002-05-16
*
suppression de inf_decidable dans ZArith_dec (pour SeachPattern)
filliatr
2002-05-16
*
Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage de
herbelin
2002-05-15
*
Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage de
herbelin
2002-05-15
*
MAJ
herbelin
2002-05-15
*
Finalement VTactic est gardé pour y plonger les tactiques ML, le
herbelin
2002-05-15
*
- abstract_sum_scalar, plus_sum_scalar and minus_sum_scalar were bogus
barras
2002-05-15
*
Contournement de la fermeture ML dans VContext
herbelin
2002-05-15
*
MAJ
herbelin
2002-05-15
*
MAJ V7.3
herbelin
2002-05-15
*
maj
filliatr
2002-05-15
*
mention -dump-glob
filliatr
2002-05-15
*
MAJ
herbelin
2002-05-14
*
- Changement de l'ordre de filtrage dans "Match Context"
herbelin
2002-05-14
*
Utilisation d'une construction spéciale SECVAR pour gérer la
herbelin
2002-05-14
*
petite erreur de syntaxe
barras
2002-05-14
*
modification de clenv_merge:
barras
2002-05-14
*
Ajout de la modification des sortes d'elimination
mohring
2002-05-14
*
ajout des theoremes eqT_rec_r et eqT_rect_r pour Rewrite
barras
2002-05-14
*
Changement de eq en eqT comme equivalence de setoide par defaut.
clrenard
2002-05-14
[next]