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
*
*** 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
*
petit nettoyage de kernel/inductive
barras
2002-02-07
*
Ajout tactiques Rename et Pose; modifications pour Inversion
herbelin
2002-02-01
*
changement generation de schema d'elimination, False_rec est primitif, Constr...
mohring
2002-01-31
*
Remplacement cut_intro par true_cut_anon pour Inversion
herbelin
2002-01-25
*
Bug calcul de la signature incorrecte en présence de letin
herbelin
2002-01-25
*
Remplacement cut_intro par true_cut_anon
herbelin
2002-01-24
*
Bug calcul de la signature incorrecte en présence de letin
herbelin
2002-01-24
*
Bug dépendances en les corps des let-in oubliées
herbelin
2002-01-24
*
Mise de Intros id au format de Intro en forçant aussi la réduction si demandé
herbelin
2002-01-15
*
Mise en place de la réduction sous forme d'implications d'atomes en fn de tête
herbelin
2001-12-20
*
Utilisation de Hnf plutôt que Red
herbelin
2001-12-20
*
Puisque Orelse semble lier moins que THEN, ajout d'un reduce après le Orelse
herbelin
2001-12-19
*
Insertion de Red sur chaque atome dans Tauto et Intuition
herbelin
2001-12-19
*
Tentative d'amélioration du résultat de Intuition
herbelin
2001-12-19
*
coq-bugs #12: probleme de metamap resolu
barras
2001-12-18
*
compat ocaml 3.03
filliatr
2001-12-13
*
Parade contre effet indésirable du commit précédent
herbelin
2001-12-06
*
Amélioration nommage hypothèses NewInduction (et incompatibilités)
herbelin
2001-12-06
*
desobfuscation du code de la verif de la condition de garde
barras
2001-11-30
*
nouvel algo de conversion plus uniforme
barras
2001-11-29
*
Fusion de declare/add_constant, declare/add_parameter et add_discharged_constant
herbelin
2001-11-20
*
Diverses petites simplications de la machine de preuves.
clrenard
2001-11-19
*
Suppression des stamps et donc des *_constraints
clrenard
2001-11-12
*
Suites modifs du noyau. Univ devient purement fonctionnel.
barras
2001-11-12
*
Suite de la suppression : enamed_declaration est remplace par evar_map.
clrenard
2001-11-06
*
Suppression des local_constraints, des ctxtty et du focus.
clrenard
2001-11-06
*
GROS COMMIT:
barras
2001-11-05
*
Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR
delahaye
2001-10-23
*
Bug Induction (prise en compte let-in + ordre des dépendances dans thin)
herbelin
2001-10-23
*
Export hide_ident_or_numarg_tactic
herbelin
2001-10-15
*
Prise en compte Intros until dans Discriminate, Injection et Simplify_eq + ne...
herbelin
2001-10-15
*
Suppression option immediate_discharge; nettoyage de Declare et conséquences
herbelin
2001-10-11
*
Incompatibilité entre la prise en compte des univers au niveau des tactiques...
herbelin
2001-10-10
*
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-10-09
*
Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'Cle...
herbelin
2001-10-05
[next]