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
*
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
*
Ajout du printer de tactiques + modif du Dynamic ocaml
delahaye
2001-09-30
*
make doc
filliatr
2001-09-21
*
Correction (double) bug de Generalize Dependent
herbelin
2001-09-20
*
Transparent
barras
2001-09-20
*
let-in dans Refine
filliatr
2001-09-20
*
Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles de...
herbelin
2001-09-19
*
Deplacement des setoides.
clrenard
2001-09-19
*
Modification de l'emplacement des fichiers pour les setoides.
clrenard
2001-09-18
*
Ajout syntaxe "Assert H:T."
herbelin
2001-09-14
*
eclaircissement du code
courant
2001-09-13
*
Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...
herbelin
2001-09-10
*
Nettoyage reduce_to_ind et one_step_reduce
herbelin
2001-09-09
*
Préparation à la mise en place d'univers algébriques
herbelin
2001-09-09
*
Correction d'un bug de pretty-print.
clrenard
2001-09-03
*
Change la constante d'entree de Immediate
mohring
2001-08-28
*
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
[next]