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
*
Correction bug Tauto : la regle pour (A->B)->C echouait quand C etait
courant
2002-07-15
*
Que la localisation des erreurs pour les tactiques atomiques marche
herbelin
2002-07-11
*
Hack pour autoriser les $n dans les Grammar tactic
herbelin
2002-07-03
*
Réparation de l'interprétation des fermetures (sans casser Field!)
herbelin
2002-06-13
*
Ajout coercion constr vers hyp quantifiée
herbelin
2002-06-06
*
Tentative de réparation d'un bug Omega: une variable de section qui après e...
herbelin
2002-06-06
*
Passage de PatternMatchingFailure vers UserError pour capture par tclFIRST
herbelin
2002-06-06
*
Repercussion de la possibilit de mettre des hyps quantifiees dans Simplify_eq...
herbelin
2002-06-05
*
Rpercussion de la possibilit de mettre des hyps quantifies dans Simplify_eq e...
herbelin
2002-06-05
*
Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar...
herbelin
2002-06-05
*
Les VContext ne sont plus des fermetures (temporaire)
delahaye
2002-05-31
*
Nettoyage
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
*
Fichiers tactics/*.ml4 remplacent les tactics/*.v
herbelin
2002-05-29
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
Réorganisation des tclTHEN (cf dev/changements.txt)
herbelin
2002-05-29
*
Fichiers tactics/*.ml4 remplacent les tactics/*.v
herbelin
2002-05-29
*
Pour les tactiques dépendant de False
herbelin
2002-05-29
*
Correction of a bug in Intuition (no more decomposition of dependent pairs).
corbinea
2002-05-22
*
Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage de
herbelin
2002-05-15
*
Finalement VTactic est gardé pour y plonger les tactiques ML, le
herbelin
2002-05-15
*
- Changement de l'ordre de filtrage dans "Match Context"
herbelin
2002-05-14
*
ajout des theoremes eqT_rec_r et eqT_rect_r pour Rewrite
barras
2002-05-14
*
Changement de eq en eqT comme equivalence de setoide par defaut.
clrenard
2002-05-14
*
Minor correction of get_lem_name
coq
2002-05-02
*
nettoyage code
courant
2002-05-02
*
Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.ml
herbelin
2002-04-11
*
*** empty log message ***
courant
2002-04-08
*
- modifs de la condition de garde pour mieux tenir compte des raisonnements
barras
2002-04-02
*
Simplification de Proof_type.prim_rule
herbelin
2002-03-27
*
Prise en compte des dependances dans la tactique Case
mohring
2002-03-26
*
Intuition ne fait plus de Unfold des constantes (il faut les faire
courant
2002-03-21
*
Intuition now takes an (optional) tactic as parameter. This tactic is
courant
2002-03-20
*
Tauto est maintenant stable par "Intro" :
courant
2002-03-15
*
*** empty log message ***
mohring
2002-03-13
*
Simplify_eq echouait sur des hypotheses trivial comme O=O
barras
2002-03-07
*
*** empty log message ***
barras
2002-03-05
*
assert failure avec Conditional Rewrite
barras
2002-03-05
*
suppression de code mort
barras
2002-03-05
*
Nouveau Rewrite-in plus economique
barras
2002-03-04
*
labels appliques dans un ordre incorrect
barras
2002-03-01
*
Uniformisation convert_hyp; correction problème de dépendance dans letin_tac
herbelin
2002-02-28
*
suppression de pop_named
barras
2002-02-22
*
Elim dependente n'appelait pas la bonne fonction pour calculer le predicat
barras
2002-02-19
*
but de CutRewrite <- (assert false)
barras
2002-02-18
*
petits changements cosmetiques sur les tactiques
barras
2002-02-15
*
- Reforme de la gestion des args recursifs (via arbres reguliers)
barras
2002-02-14
*
substitution et pattern modulo let
barras
2002-02-11
*
mauvais comportement de l'inversion vis-a-vis des lets
barras
2002-02-08
[next]