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 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
*
nouvelle implantation de la reduction
barras
2001-03-01
*
modif
mohring
2001-02-28
*
EAuto mixte (largeur puis profondeur)
mohring
2001-02-27
*
changement message d'erreur Abstract
filliatr
2001-02-26
*
Eauto version en largeur
mohring
2001-02-26
*
Abstract: on échoue si le but contient des existentielles
filliatr
2001-02-26
*
ident au lieu de string pour le nom de base de qualid
herbelin
2001-02-16
*
Prise en compte noms longs dans SuperAuto
herbelin
2001-02-16
*
Mise en place d'un système optionnel de discharge immédiat; prise en compte...
herbelin
2001-02-14
*
Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...
herbelin
2001-02-14
*
Bug affichage
herbelin
2001-02-14
*
Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...
herbelin
2001-02-14
*
code mort
herbelin
2001-02-07
*
EqDecide
filliatr
2001-02-06
*
Ajout d'une heuristique pour les types dependants
delahaye
2001-02-05
*
Message d'erreur plus explicite pour Tauto
delahaye
2001-02-05
*
rétablissement nouveau Tauto
filliatr
2001-02-05
*
Résolution d'un bug de simplification
delahaye
2001-02-03
*
application patch Cuit Alvarado : tclTHENSi et intros_until_n exportés
filliatr
2001-02-01
*
oubli de Closure.EvalConstRef
filliatr
2001-02-01
*
- coqc : option -image
filliatr
2001-02-01
*
Mise en place de la possibilite d'unfolder des variables locales et des const...
filliatr
2001-01-31
*
Bug fixed: the case [ id : ?1 -> ?2 |- ?] was missing in tauto_main
sacerdot
2001-01-30
*
As an heuristic, now both in tauto and intuition we try to avoid the initial
sacerdot
2001-01-29
*
Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...
herbelin
2001-01-24
*
Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...
herbelin
2001-01-24
[prev]
[next]