index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
interp
Commit message (
Expand
)
Author
Age
*
Ajout d'une option de débogage pour expliciter l'instance des evars
herbelin
2007-01-11
*
Suite commit restructuration discharge (application du type de
herbelin
2007-01-10
*
Nouvelle approche pour le discharge modulaire
herbelin
2007-01-10
*
Addition of a "Combined Scheme" vernacular command for building the conjuncti...
msozeau
2006-12-23
*
Variable print_instances pour déboguer les instances d'evar
herbelin
2006-12-12
*
Pas d'escamotage des noms réservés si Set Printing All actibvé
herbelin
2006-12-08
*
Remplacement de la dépendance de G_vernac en G_constr (source
herbelin
2006-12-03
*
Suppression du type 'tac dans les abstract_argument_type: devenu inutile
herbelin
2006-11-20
*
Add a flush for a warning.
courtieu
2006-10-23
*
Notations:
herbelin
2006-10-09
*
Annulation de l'essai de changement de sémantique du %scope (révision 9208).
herbelin
2006-10-06
*
Essai de changement de sémantique du %scope :
herbelin
2006-10-05
*
Tentative d'amélioration du message d'erreur en cas de paramètre non laissé
herbelin
2006-09-24
*
Correction bug dans détection clause "in" mal formée quand le "in" est
herbelin
2006-09-24
*
Correction bug #1179 (result of Notation.decompose_notation_key in wrong order
herbelin
2006-09-23
*
- Correction filtrage des notations impliquant un "match" : la présence
herbelin
2006-09-23
*
Protection List.fold_left2 (cf bug #1224)
herbelin
2006-09-22
*
Declarative Proof Language: main commit
corbinea
2006-09-20
*
Export de fonctions d'interprétation acceptant des evars non résolues
herbelin
2006-09-01
*
Correction bug 1172 + correction en passant de la taille des paramètres de f...
herbelin
2006-07-07
*
Extension des motifs disjonctifs au cas de disjonction de motifs multiples
herbelin
2006-07-03
*
documentation
herbelin
2006-06-23
*
Légère mise à jour
herbelin
2006-06-22
*
Added {measure x f} as a valid recursion order.
msozeau
2006-06-22
*
Changement du type d'argument 'TacticArgType X' en un type
herbelin
2006-06-08
*
Réinitialisation de token_number à chaque compilation d'un nouveau fichier ...
notin
2006-06-08
*
Correction trou de subject-reduction de create_arg dans genarg.mli
herbelin
2006-06-07
*
Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...
herbelin
2006-05-30
*
The "clean integration of subtac" patch.
msozeau
2006-05-29
*
- Déplacement des types paramétriques prod, sum, option, identity,
herbelin
2006-05-28
*
Adaptation de Coqdoc au nouveau add_glob
notin
2006-05-24
*
Retour version 8852 de constrintern.ml
herbelin
2006-05-23
*
Erreur commit constrintern.ml
herbelin
2006-05-23
*
Changement de précédence de l'argument du by de assert; conséquences...
herbelin
2006-05-23
*
Modification de add_glob (support des modules dans Coqdoc)
notin
2006-05-23
*
Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsort
herbelin
2006-05-19
*
r8931@thot: notin | 2006-04-28 16:19:38 +0200
notin
2006-04-28
*
Typo dans précédent commit (8755); protection renforcée dans analyse claus...
herbelin
2006-04-28
*
- Distinction explicite des parties paramètres et arguments dans le type
herbelin
2006-04-27
*
Standardisation nom option_app en option_map
herbelin
2006-04-27
*
préparation de add_glob en vue d'isolement de la partie module pour
herbelin
2006-04-27
*
- Utilisation d'abbréviations pour les types intervenant dans RCases
herbelin
2006-04-26
*
Timide tentative de clarification du statut de l'opérateur de filtrage
herbelin
2006-04-24
*
Si un fixpoint a plusieurs arguments, mais un seul de type inductif,
letouzey
2006-04-14
*
- Documentation of the Program tactics.
msozeau
2006-04-07
*
Amendement impression evar pour affichage des Meta par 'info'
herbelin
2006-03-31
*
Made pretyping a functor over a coercion implementation. Pretyping.Default us...
msozeau
2006-03-22
*
- Correction bug calcul mind_consnrealargs, introduit à la révision
herbelin
2006-03-22
*
Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.
msozeau
2006-03-13
*
Correction message d'erreur ltac et adoption du modèle de message de Tacinterp
herbelin
2006-03-04
[next]