index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
Commit message (
Expand
)
Author
Age
...
*
Add a parameter to QuestionMark evar kind to say it can be turned into an obl...
msozeau
2007-03-19
*
Suppression argument pattern_source du case_info (code jamais utilisé)
herbelin
2007-03-15
*
Ajout fonction clenv_conv_leq pour résoudre les pbs de la forme
herbelin
2007-02-22
*
Utilisation de l'environnement pour l'affichage de certains messages d'erreurs
herbelin
2007-02-21
*
Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGES
herbelin
2007-02-21
*
Add functionality to permit printing terms with references to anonymous varia...
msozeau
2007-02-16
*
Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de
herbelin
2007-02-13
*
Correction d'un bug dans check_and_clear_in_constr + simplification de
notin
2007-01-31
*
Nouvelle implantation de clear_hyps
notin
2007-01-30
*
correction d'un bug d'efficacite dans le printer
jforest
2007-01-26
*
Correction du bug #1315:
notin
2007-01-22
*
Correction d'un bug d'unification-pattern dans l'algo d'unification
herbelin
2007-01-22
*
Correction pour le rapport de bug #1325 par rétablissement du
herbelin
2007-01-22
*
Protection contre les warnings 'unused variable' de ocaml 3.09
herbelin
2007-01-19
*
Rework subtac pattern matching equalities generation.
msozeau
2007-01-02
*
Protection contre une source possible de liaison de lambda anonyme
herbelin
2006-12-29
*
Confusion sur le paramètre à donner à concrete_name lors du commit 9450
herbelin
2006-12-14
*
Alignement de la politique de renommage de rename_bound_var (utilisé pour
herbelin
2006-12-13
*
Correction du bug #1273, deuxième version (avec des shémas d'elimination pl...
notin
2006-12-12
*
Correction du bug #1273 (problème avec les paramètres non récursivement un...
notin
2006-12-12
*
Backtrack sur suppression des vars anonymes des contextes d'evars (echec Case...
herbelin
2006-12-12
*
Correction bug #1041 (double cause : non évitement des noms existants en
herbelin
2006-12-12
*
Évitement des noms de constructeurs dans les motifs de filtrage de "match"
herbelin
2006-12-09
*
correction du bug : VM value extraction error (PR#1290)
bgregoir
2006-11-29
*
Code mort découvert par Matthieu
herbelin
2006-11-22
*
Dépendance inutile en Tacexpr, de proofs, qui se compile en principe après
herbelin
2006-11-19
*
Raffinement de l'unification de "apply": mémorisation de certains
herbelin
2006-11-19
*
Code mort (duplication de code dans reductionops.ml)
herbelin
2006-11-18
*
Suppression source de complexité polynomiale introduite par le polymorphisme
herbelin
2006-11-03
*
Compatibilité du polymorphisme de constantes avec les sections.
herbelin
2006-10-29
*
Extension du polymorphisme de sorte au cas des définitions dans Type.
herbelin
2006-10-28
*
Applatissement des noeuds application vide dans le filtrage Ltac (ex:
herbelin
2006-10-25
*
Suite commit 9277
herbelin
2006-10-25
*
Correction d'une tentative incorrecte (révision 9266) de clarification
herbelin
2006-10-25
*
Ajout de la tactique "apply in".
herbelin
2006-10-24
*
Le calcul de la classe dans class_args_of ne suivait pas celui de class_of
herbelin
2006-10-21
*
Correction d'un vieux bug de coercion avec éta-expansion (utilisation
herbelin
2006-10-21
*
Notations:
herbelin
2006-10-09
*
Remplacement des nf_evar (source de complexité polynomiale) par de la
herbelin
2006-10-06
*
Déplacement de on_judgment_type de Typeops vers Termops
herbelin
2006-10-06
*
Suppression d'une source de complexité polynomiale dans le pretypage
herbelin
2006-10-06
*
Correction d'un bug dans l'unification: lors de l'unification d'un meta m et ...
notin
2006-10-05
*
Correction de deux cas où les types inductifs n'étaient pas comparés
herbelin
2006-10-05
*
Ajout allowed_sorts
herbelin
2006-10-01
*
Correction d'un bug de coercion de pattern introduit dans la 8.1beta
herbelin
2006-09-23
*
Correction bug #1168 (dans les coercions de pattern, c'est le nombre
herbelin
2006-09-23
*
Wish #1187 granted (support for canonical structures that are records
herbelin
2006-09-23
*
Declarative Proof Language: main commit
corbinea
2006-09-20
*
Report de l'heuristique d'unification premier ordre flexible/rigide
herbelin
2006-09-15
*
Débogage: ajout affichage contraintes d'unification
herbelin
2006-09-15
[prev]
[next]