index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
proofs
Commit message (
Expand
)
Author
Age
...
*
unification avec TOUS les sous-termes ( (plus ?) ne s'unifiait pas avec les
barras
2001-09-17
*
exceptions
barras
2001-09-14
*
Un conv aurait dû être un conv_leq
herbelin
2001-09-10
*
Nettoyage reduce_to_ind et one_step_reduce
herbelin
2001-09-09
*
Suppression du retypage dans w_Declare
herbelin
2001-09-09
*
Parsing
herbelin
2001-08-10
*
Ajout nf_betaiota dans le cut interne
herbelin
2001-08-08
*
Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ...
herbelin
2001-08-07
*
Code mort
herbelin
2001-08-05
*
Suppression de l'affichage du non-reparsable 'Local constraint change'
herbelin
2001-07-24
*
Changements dans le traitement des qualid's
delahaye
2001-07-19
*
Evar et Zeta ne sont plus implicites dans Delta (mais le restent dans Compute...
herbelin
2001-07-02
*
Nettoyage/restructuration des ensembles d'indicateurs de réductions
herbelin
2001-07-02
*
Autoriser Apply avec un but sous forme d'implication ou de quantification
barras
2001-06-29
*
Backtracking pour le Match
delahaye
2001-06-29
*
Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...
herbelin
2001-06-25
*
Extension des parametres de Clear + Inst
delahaye
2001-06-19
*
Interpretation MetaId + Progress + Inst
delahaye
2001-06-18
*
Pretty -> Prettyp
filliatr
2001-05-28
*
amelioration des messages d'erreurs vis a vis des evars
barras
2001-05-23
*
Erreur dans un commentaire ...
clrenard
2001-05-18
*
quelques bug reports mineurs
barras
2001-05-07
*
Changement de la structure des points fixes
barras
2001-05-03
*
Metas dans les Unfold's
delahaye
2001-04-19
*
Reparation du bug de Try
delahaye
2001-04-14
*
Ajout de _ dans les patterns d'intro
mohring
2001-04-12
*
utilisation de Options.if_verbose
filliatr
2001-04-03
*
amelioration de la structure des univers
barras
2001-03-28
*
entetes
filliatr
2001-03-15
*
module Explore générique et réécriture EAuto avec ce module; occur check ...
filliatr
2001-03-05
*
Déplacement de qualid dans Nametab, hors du noyau
herbelin
2001-03-01
*
backtrack unification types et deplacement make_clenv_binding
filliatr
2001-03-01
*
introduction d'un refine avec resolution des types et de l'instantiation des ...
mohring
2001-02-28
*
ident au lieu de string pour le nom de base de qualid
herbelin
2001-02-16
*
Prise en compte noms longs dans SuperAuto
herbelin
2001-02-16
*
Obsolète (cf Coqlib)
herbelin
2001-02-14
*
simplification du make depend; fonctions de stat. util. memoire dans certains...
filliatr
2001-02-08
*
exporting traverse_to and mutate: they are used in pcoq.
bertot
2001-02-08
*
Reparation du pretty-print pour les tactiques
delahaye
2001-02-07
*
Correction pour les Unfold/Fold dans Cbv
delahaye
2001-02-06
*
application patch Cuit Alvarado : tclTHENSi et intros_until_n exportés
filliatr
2001-02-01
*
*** empty log message ***
mohring
2001-02-01
*
Mise en place de la possibilite d'unfolder des variables locales et des const...
filliatr
2001-01-31
*
make doc
herbelin
2001-01-27
*
Retour en arrière sur le pb f_equal en attente meilleure solution
herbelin
2001-01-22
*
Bug « f_equal » : arguments inférables par une unification des types qui n...
herbelin
2001-01-21
*
Meta Definition + Tactic Definition
delahaye
2001-01-09
*
Arite cachee de Match Context + Meta Definition
delahaye
2001-01-05
*
Ajout du Let pour le langage de tactiques
delahaye
2000-12-29
*
Elimination des coupures
herbelin
2000-12-26
[prev]
[next]