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
*
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
*
coqide: toolbar/autosave
monate
2003-05-07
*
Localisation erreurs TacAlias; Globalisation moins tolérante dans les
herbelin
2003-04-28
*
Localisation des appels de tactiques définies sans arguments
herbelin
2003-04-14
*
Affichage des tactiques en v8
herbelin
2003-04-07
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07
*
Ajout d'un message à FailTac
herbelin
2003-03-31
*
Réparation bug de l'unification. En effet, avant l'instanciation d'une evar
clrenard
2003-03-28
*
*** empty log message ***
barras
2003-03-12
*
Debugger plus informatif
delahaye
2003-02-13
*
Bug Rename
herbelin
2003-02-08
*
Pour satisfaire ProofGeneral
coq
2003-01-31
*
Plus du tout de backtracking dans "Match term"; vrai Exit dans débogueur
herbelin
2003-01-21
*
Restructuration interpréteur de tactique: plus d'évaluation partielle à la...
herbelin
2003-01-19
*
Erreur sur precedent commit
herbelin
2003-01-19
*
Restructuration interpréteur de tactique: plus d'évaluation partielle à la...
herbelin
2003-01-19
*
Amélioration choix des noms dans abstract_list_all
herbelin
2002-12-30
*
code mort
herbelin
2002-12-24
*
Tentative d'interdire les K-abstractions si allow_K est faux et le
herbelin
2002-12-23
*
Cas motif universel
herbelin
2002-12-22
*
Légère amélioration des messages d'erreur des with-bindings et des Rewrite
herbelin
2002-12-21
*
code mort
herbelin
2002-12-21
*
Prise en compte des coercions dans les 'with' bindings
herbelin
2002-12-20
*
simplification de solve_subgoal: n'utilise plus frontier
barras
2002-12-19
*
suite du commit precedent
barras
2002-12-19
*
Compensation de suppression betaiota de type_of (suite)
herbelin
2002-12-13
*
Compensation de suppression betaiota de type_of (suite)
herbelin
2002-12-12
*
Ajout du vernac Proof with
gregoire
2002-12-12
*
Compensation de suppression betaiota de type_of
herbelin
2002-12-11
[next]