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
*
Standardisation du nom des méthodes de Evd
herbelin
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
*
- Utilisation d'abbréviations pour les types intervenant dans RCases
herbelin
2006-04-26
*
Reverting nf_betaiotaevar_preserving_vm_cast
jforest
2006-04-25
*
Code mort (suite)
herbelin
2006-04-25
*
Suppression code mort
herbelin
2006-04-25
*
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
*
Pas fier
herbelin
2006-04-14
*
replacing whd_betaiotaevar_preserving_vm_cast
jforest
2006-04-14
*
Fixes for new unification, not used in default version as it really changes u...
msozeau
2006-04-10
*
Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous...
msozeau
2006-04-10
*
- Documentation of the Program tactics.
msozeau
2006-04-07
*
Inductifs avec polymorphisme de sorte (version initiale)
herbelin
2006-03-29
*
Correction bug/typo dans splay_prod_assum et ajout decomp_sort
herbelin
2006-03-28
*
Subtac fixes, single fixpoint definitions are working again. Added a toggle o...
msozeau
2006-03-22
*
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
*
Modification des propriétés (svn:executable)
notin
2006-03-17
*
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
*
Correctif pour bug #1089 (cannot define an isevar twice)
herbelin
2006-03-02
*
Localisation des erreurs de sorte du prétypage
herbelin
2006-02-08
*
oubli de code de debugging
herbelin
2006-02-07
*
Amélioration des messages d'erreurs de tacred; unfold considère maintenant le
herbelin
2006-02-07
*
Mise en conformité de l'ordre des occurrences de pattern avec l'affichage
herbelin
2006-02-07
*
Optimisation filtrage sans lieurs (utile pour Ltac)
herbelin
2006-02-01
*
Suppression fonctions d'interprétation du vieux Case
herbelin
2006-01-30
*
Gestion des erreurs pour nombre incorrect d'argument des constructeurs (et de
herbelin
2006-01-30
*
- Prise en compte de la clause 'in I' pour coercer le type du terme à filtrer
herbelin
2006-01-30
*
Fonctions retournant les arits des constructeurs et inductifs (suite)
herbelin
2006-01-30
*
Fonctions retournant les arits des constructeurs et inductifs
herbelin
2006-01-30
*
- Prise en compte de la clause 'in I' pour coercer le type du terme à filtrer;
herbelin
2006-01-30
*
Documentation
herbelin
2006-01-29
*
Version préliminaire d'inversion de la compilation du filtrage
herbelin
2006-01-16
*
Standardisation du nom de subst_raw en subst_rawconstr
herbelin
2006-01-11
*
Restructuration et simplification des fonctions d'affichage, de détypage
herbelin
2006-01-11
*
Suppression résidus code v7 et traducteur
herbelin
2006-01-11
*
Ajout de la longueur de l'arité des constructeurs dans one_inductive_body et...
herbelin
2006-01-10
*
Fonctions de conversion rawconstr <-> cases_pattern
herbelin
2006-01-08
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-26
*
Restructuration des points d'entrée de Pretyping et Constrintern
herbelin
2005-12-21
*
Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...
herbelin
2005-12-17
*
Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...
herbelin
2005-12-17
*
Orthographe de 'instantiate'
herbelin
2005-12-17
*
changement d'egalite pour le named_context_val
gregoire
2005-12-05
*
Changement des named_context
gregoire
2005-12-02
*
parametres inductifs
mohring
2005-11-28
[next]