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
*
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
*
Remplacement de debug en assert
herbelin
2000-12-25
*
Code mort
herbelin
2000-12-20
*
Bug dans l'utilisation de l'option debug
herbelin
2000-12-20
*
Bug norm_evar_pf; remplacement par l'insertion d'un noeud local_constraints q...
herbelin
2000-12-20
*
Ajout set_lc
herbelin
2000-12-20
*
Correction pour les variables abstraites dans les Tactic Definitions
delahaye
2000-12-19
*
Code mort
herbelin
2000-12-18
*
Documentation
herbelin
2000-12-18
*
Redondant or incompatible instantiations in clenv_assign now correctly trapped
herbelin
2000-12-16
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
Hint Unfold Local + commentaires
mohring
2000-12-12
*
Ajout erreur DoesNotOccurIn
herbelin
2000-12-06
*
Prise en compte Let dans le calcul des arguments manquants d'un lemme (clenv_...
herbelin
2000-12-05
*
Portage d'AutoRewrite
delahaye
2000-12-02
*
Elimination du '
delahaye
2000-11-28
*
Ajout de evaluable_named_decl et evaluable_rel_decl en parallele au evaluable...
herbelin
2000-11-27
*
Branchement du mécanisme d'instantiation des Evar en présence de définitio...
herbelin
2000-11-27
*
certains effets disparaissent a la sortie des sections, d'autres non (selon S...
filliatr
2000-11-24
*
Correction d'un bug lorsque des Variables sont clearees dans le but courant
delahaye
2000-11-23
*
print_id, print_sp -> pr_id, pr_sp
herbelin
2000-11-23
*
Affichage des paths avec des '.', 2eme; prise en compte qualid
herbelin
2000-11-23
[next]