index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
tacred.ml
Commit message (
Expand
)
Author
Age
*
Standardisation nom option_app en option_map
herbelin
2006-04-27
*
Amélioration des messages d'erreurs de tacred; unfold considère maintenant le
herbelin
2006-02-07
*
Changement des named_context
gregoire
2005-12-02
*
Nettoyage suite à la détection par défaut des variables inutilisées par o...
herbelin
2005-11-08
*
Correction bug invert_names (cf bug #1031)
herbelin
2005-11-02
*
Adoption du nom canonique global_of_constr pour éviter confusion avec type r...
herbelin
2005-05-20
*
Uniformisation de destApplication en destApp
herbelin
2005-02-12
*
Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...
herbelin
2005-01-02
*
ExtraRedExpr maintenant sans argument: pas très souple mais au moins convien...
herbelin
2004-12-29
*
UserError in reduce_to_*_ref
herbelin
2004-11-29
*
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
sacerdot
2004-11-16
*
Changement dans les boxed values .
gregoire
2004-11-12
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
Vérification de la typability de 'pattern'
herbelin
2004-10-17
*
Un bug de simpl de 1995 + nettoyage (les args de list_fold_left_i etaient inc...
herbelin
2004-09-08
*
premiere reorganisation de l\'unification
barras
2004-09-03
*
Nouvelle en-tête
herbelin
2004-07-16
*
Essai de suppression de eta dans simpl (cf bug #779)
herbelin
2004-06-29
*
Terminologie plus intuitive: evaluable -> unfoldable
herbelin
2004-04-30
*
bug #606: mis un message d'erreur plus clair
barras
2004-04-07
*
Bug numerotation des occurrences pour 'simpl id at n' (suite)
herbelin
2004-02-13
*
Bug numerotation des occurrences pour 'simpl id at n' (2 protections maintena...
herbelin
2004-02-13
*
Bug (destruct/induction ne savent pas traiter le cas non atomique avec paramÃ...
herbelin
2004-01-27
*
Affichage opaque
herbelin
2003-12-23
*
Prise en compte des sous-termes imbriqués pour 'simpl ident at nums'
herbelin
2003-12-17
*
Bug introduit avec le 'Simpl f'
herbelin
2003-11-22
*
Ajout 'Simpl f'
herbelin
2003-11-21
*
Ajout reduce_to_quantified_ref
herbelin
2003-11-09
*
Correction du bug 335 et Export/Require Export dans un module
coq
2003-10-07
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...
letouzey
2003-04-16
*
*** empty log message ***
barras
2003-03-12
*
Ajout Simpl et Change sur des sous-termes
herbelin
2002-12-09
*
retour en arriere concernant la recherche d'occurence modulo expansion des le...
barras
2002-10-09
*
correction de bugs:
barras
2002-08-16
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
Mise au point de declare_red_expr
herbelin
2002-05-30
*
Finalement un seul constr pour l'instant dans ExtraRedExpr
herbelin
2002-05-30
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
petits changements cosmetiques sur les tactiques
barras
2002-02-15
*
Non dépliage des Fix non réductibles dans Hnf
herbelin
2001-12-20
*
compat ocaml 3.03
filliatr
2001-12-13
*
nouvel algo de conversion plus uniforme
barras
2001-11-29
*
GROS COMMIT:
barras
2001-11-05
*
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-10-09
*
Transparent
barras
2001-09-20
*
Nettoyage reduce_to_ind et one_step_reduce
herbelin
2001-09-09
*
Extension à Cases et Fix de la réduction pas à pas vers un produit (Red)
herbelin
2001-09-07
*
Bug Simpl
herbelin
2001-07-24
*
Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...
herbelin
2001-07-21
[next]