index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
Commit message (
Expand
)
Author
Age
*
Parsing
herbelin
2001-08-10
*
Renommage TrueCut -> Assert
herbelin
2001-08-08
*
La grammaire n'était plus LL1
herbelin
2001-08-08
*
Modification Tauto pour qu'il puisse destructurer des hypotheses de la forme
courant
2001-08-08
*
Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ...
herbelin
2001-08-07
*
Remplacement de 'clause' par 'hyps' pour les tactiques qui ne peuvent pas s'a...
herbelin
2001-08-05
*
Elimination des coupures quand les 'clause' se réduisent à des hypothèses,...
herbelin
2001-08-05
*
Remplacement de 'clause' par 'hyps' pour les tactiques qui ne peuvent pas s'a...
herbelin
2001-08-05
*
Mise en place d'un nouveau Destruct sur le modèle du nouvel Induction
herbelin
2001-08-05
*
Suppression des TmpHyp disgracieuses dans Decompose; utilisation de combinate...
herbelin
2001-08-05
*
Elimination des coupures quand les 'clause' se réduisent à des hypothèses,...
herbelin
2001-08-05
*
Ajout code pour un Destruct similaire au NewInduction
herbelin
2001-08-01
*
Branchement de induction/destruct sur intros_until_n (intros_do obsolete ne p...
herbelin
2001-07-13
*
Branchement sur bad_tactic_args
herbelin
2001-07-10
*
Branchement sur bad_tactic_args
herbelin
2001-07-10
*
Ajout du .ml pour la tactique Setoid_replace
clrenard
2001-07-10
*
Changement de place de la tactique Setoid_rewrite et renommage
clrenard
2001-07-10
*
ajout Show Intro(s)
letouzey
2001-07-04
*
Autoriser Apply avec un but sous forme d'implication ou de quantification
barras
2001-06-29
*
traitement du let dans red_product (tactique Red)
barras
2001-06-29
*
commit d'un bug de Apply.
barras
2001-06-27
*
Refine sur les CoFix
filliatr
2001-06-25
*
Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...
herbelin
2001-06-25
*
Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...
herbelin
2001-06-25
*
Fix d'un bug de Tauto
delahaye
2001-06-15
*
Prise en compte env local (et defs locales) dans Change
herbelin
2001-06-13
*
Correction d'un bug du a un Intros trop violent
delahaye
2001-06-01
*
Backtrack vers comportement de la V6 pour eviter les globaux dans le nommage ...
herbelin
2001-06-01
*
Amelioration - subjective - de l'affichage des Hint
herbelin
2001-05-31
*
Pretty -> Prettyp
filliatr
2001-05-28
*
Remplacement push_rec_types (Rel) pour Fix parpush_named_rec_types
herbelin
2001-05-25
*
amelioration des messages d'erreurs vis a vis des evars
barras
2001-05-23
*
Changement de la structure des points fixes
barras
2001-05-03
*
Ajout du cas True->A|-B
delahaye
2001-04-24
*
Fonction lookup enlevee
delahaye
2001-04-19
*
Mise en page
herbelin
2001-04-15
*
Ajout de _ dans les patterns d'intro
mohring
2001-04-12
*
Mis un message d'erreur explicite pour l'echec de Elim en cas
mohring
2001-04-12
*
Make it possible to perform proofs by induction even on non-inductive types,
bertot
2001-04-03
*
amelioration de la structure des univers
barras
2001-03-28
*
Problèmes de NewInduction
herbelin
2001-03-22
*
entetes
filliatr
2001-03-15
*
bug de refine: uncaught exception Array.sub
barras
2001-03-09
*
changement comparaison etats
filliatr
2001-03-08
*
Modification de e_give_exact pour eviter d'echouer sur l'unification
mohring
2001-03-06
*
eta-expansion
mohring
2001-03-06
*
EAutod (debug)
filliatr
2001-03-06
*
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
[next]