index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
proofs
Commit message (
Expand
)
Author
Age
...
*
deplacement de clenv vers pretyping
barras
2004-09-03
*
premiere reorganisation de l\'unification
barras
2004-09-03
*
Nouvelle en-tête
herbelin
2004-07-16
*
bugs #667 and #783 (mimick_evar and loc_table on large files)
barras
2004-07-13
*
bypass w_Define when w_refine-ing
corbinea
2004-07-07
*
updated printing of evar context (may loop ?)
corbinea
2004-06-30
*
moved instantiate binding to extratactics
corbinea
2004-06-29
*
more evar stuff
corbinea
2004-06-28
*
effective evar refining
corbinea
2004-06-26
*
Amélioration message d'erreur quand échec unification
clrenard
2004-04-20
*
Export du type de preuve en cours pour xml
herbelin
2004-03-29
*
Changement de natural en int_or_var pour 'do' et 'fail' pour paramétrisation...
herbelin
2004-03-02
*
Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...
herbelin
2004-03-02
*
Déplacement définition intro_pattern_expr dans Genarg
herbelin
2004-03-01
*
added breakpoints to help ide
corbinea
2004-02-26
*
Localisation des erreurs d'internalisation des notations de tactiques
herbelin
2004-02-12
*
bugs avec Pose et Assert
barras
2004-01-09
*
Bug affichage des metas dans un environnement avec definitions locales (bug 277)
herbelin
2003-12-19
*
Amélioration du message d'erreur "w_unify"
clrenard
2003-12-01
*
Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...
herbelin
2003-11-25
*
Prise en compte des defs syntaxiques dans is_global et global_reference qui p...
herbelin
2003-11-24
*
Amelioration du message d'erreur en cas de tentative d'instanciation
clrenard
2003-11-15
*
factorisation et generalisation des clauses
barras
2003-11-13
*
Idtac peut prendre un argument à afficher
narboux
2003-11-12
*
petits changements de syntaxe
barras
2003-11-12
*
Traduction semantique des InHyp de clause en InHypValue si local def
herbelin
2003-11-09
*
Ajout pf_apply
herbelin
2003-11-09
*
Added Instantiate ... in
corbinea
2003-11-06
*
2 espaces en trop
herbelin
2003-11-05
*
Amelioration de l'afficheur de script structure
herbelin
2003-11-05
*
nouvelle syntaxe de ltac
barras
2003-10-16
*
code mort
herbelin
2003-10-10
*
pf_get_new_id en provenance de feu wcclausenv
herbelin
2003-10-10
*
Suppression clenv_change_head que seul Wcclausenv utisait
herbelin
2003-10-10
*
Cablage en dur de inversion
herbelin
2003-10-10
*
Gestion en temps constant de la pile des Unfo; affichage des buts par Pfedit ...
herbelin
2003-10-10
*
changement nouvelle syntaxe (pt fixes)
barras
2003-10-10
*
Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...
herbelin
2003-10-08
*
Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...
herbelin
2003-09-12
*
open superflu
herbelin
2003-09-12
*
Paramétrisation vis à vis de existential_key
herbelin
2003-09-06
*
Ground update
corbinea
2003-07-08
*
Ground Update.
corbinea
2003-06-20
*
Ajout 'Symmetry in Hyp'
herbelin
2003-06-19
*
Utilisation de intro_pattern dans NewDestruct/NewInduction
herbelin
2003-06-13
*
Réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur de...
herbelin
2003-06-10
*
Ajout FreshId
herbelin
2003-05-24
*
Suppression définitive de lmatch et or_metanum dans tacinterp
herbelin
2003-05-21
*
Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...
herbelin
2003-05-21
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
[prev]
[next]