index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
tactics.ml
Commit message (
Expand
)
Author
Age
...
*
'NewDestruct using' s'applique maintenant aussi aux types non inductifs; bug ...
herbelin
2003-11-09
*
Bug Abstract en presence de LetIn; essai d'un Assumption d'abord avec alpha-c...
herbelin
2003-10-21
*
Deplacement next_global_ident_away dans Termops
herbelin
2003-10-13
*
Typo
herbelin
2003-10-10
*
Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'
herbelin
2003-10-10
*
changement nouvelle syntaxe (pt fixes)
barras
2003-10-10
*
Correction bug NewInduction pour les inductifs de type 'ordinaux'
herbelin
2003-09-23
*
Indépendance vis à vis de Declare
herbelin
2003-09-12
*
Ajout 'Symmetry in Hyp'
herbelin
2003-06-19
*
Utilisation de intro_pattern dans NewDestruct/NewInduction
herbelin
2003-06-13
*
Backtrack du commit de Christine, qui posait probleme avec FTC
letouzey
2003-04-03
*
notations <>, Assumption avec existentiel, replace term
mohring
2003-03-28
*
Un type "standardisé" pour new_hyp
herbelin
2003-01-25
*
Commentaires; optimisation
herbelin
2002-12-30
*
code mort
herbelin
2002-12-24
*
Légère amélioration des messages d'erreur des with-bindings et des Rewrite
herbelin
2002-12-21
*
Normalisation beta-iota du type du terme appliqué (fait avant dans Typing)
herbelin
2002-12-10
*
Ajout Simpl et Change sur des sous-termes
herbelin
2002-12-09
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
JMeq now treated as an equality by tactics.
courant
2002-11-14
*
Intégration des modifs de la branche mowgli :
herbelin
2002-11-05
*
Correction d'une incompatibilité de nommage introduite lors du commit précÃ...
herbelin
2002-10-22
*
Ajout d'un suffixe "as [ names ]" pour nommer manuellement les
herbelin
2002-10-21
*
NewDestruct/NewInduction acceptent l'option "using"
herbelin
2002-10-21
*
retour en arriere concernant la recherche d'occurence modulo expansion des le...
barras
2002-10-09
*
Renoncement à distinguer les types "constr" et "types"; nettoyage
herbelin
2002-08-13
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
Branchement de Assert, Pose et LetTac sur l'algo de création de noms
herbelin
2002-07-30
*
Tentative de réparation d'un bug Omega: une variable de section qui après e...
herbelin
2002-06-06
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.ml
herbelin
2002-04-11
*
Simplification de Proof_type.prim_rule
herbelin
2002-03-27
*
Prise en compte des dependances dans la tactique Case
mohring
2002-03-26
*
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
*
petits changements cosmetiques sur les tactiques
barras
2002-02-15
*
- Reforme de la gestion des args recursifs (via arbres reguliers)
barras
2002-02-14
*
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
*
Mise de Intros id au format de Intro en forçant aussi la réduction si demandé
herbelin
2002-01-15
*
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
*
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
[prev]
[next]