index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
Commit message (
Expand
)
Author
Age
...
*
Nouvelle entrée ident_or_numarg
herbelin
2001-08-06
*
Mise en place d'un nouveau Destruct sur le modèle du nouvel Induction
herbelin
2001-08-05
*
Changements dans le traitement des qualid's
delahaye
2001-07-19
*
modifs de preuves (plus simples)
mayero
2001-07-19
*
reparation regles pour parsing Coercion Local
mohring
2001-07-13
*
ajout Show Intro(s)
letouzey
2001-07-04
*
Evar et Zeta ne sont plus implicites dans Delta (mais le restent dans Compute...
herbelin
2001-07-02
*
Ajout glob_eq{,T}
herbelin
2001-07-02
*
Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...
herbelin
2001-06-25
*
Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...
herbelin
2001-06-25
*
Extension des parametres de Clear + Inst
delahaye
2001-06-19
*
Interpretation MetaId + Progress + Inst
delahaye
2001-06-18
*
Reparation d'un bug d'affichage. Les let destructurants, if, et vieux Case
clrenard
2001-06-11
*
Fix de quelques bugs syntaxiques de Ltac
delahaye
2001-06-11
*
Retablissement de minicoq
coq
2001-05-29
*
Facilites pour le debogguage des univers.
coq
2001-05-29
*
Pretty -> Prettyp
filliatr
2001-05-28
*
Changement de la structure des points fixes
barras
2001-05-03
*
message d'erreur pour rattrapper l'anomalie avec SQUASH
barras
2001-04-25
*
Amelioration affichage
herbelin
2001-04-25
*
Messages d'erreur Cases
herbelin
2001-04-24
*
Les clauses de Rec doivent prendre des tactic_atom's
delahaye
2001-04-24
*
un warning pas beau supprimmé
filliatr
2001-04-23
*
Petit menage
delahaye
2001-04-20
*
*** empty log message ***
mayero
2001-04-19
*
Essais dans Ltac
delahaye
2001-04-19
*
Bug affichage d'implicites pour les vars liees
herbelin
2001-04-15
*
Non parenthesage des applications de tactiques
delahaye
2001-04-14
*
Ajout de _ dans les patterns d'intro
mohring
2001-04-12
*
Modified searchPattern. Before this correction, constructors were overlooked,
bertot
2001-04-10
*
Uniformisation des 'Save def_tok id'
herbelin
2001-04-09
*
nettoyage d'entrees de grammaires inutiles
courant
2001-04-09
*
branchement extraction en standard (pas de Require)
filliatr
2001-04-09
*
bug Print Proof; usage coqtop/coqc
filliatr
2001-04-06
*
mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4
filliatr
2001-04-05
*
renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...
filliatr
2001-04-04
*
Add a flag to avoid sending too many warnings when reloading syntax files
bertot
2001-04-04
*
adding entry points for the arguments of the Comment command.
bertot
2001-04-04
*
Adding A command for comments, this makes it possible to have structured
bertot
2001-04-04
*
The function filter_by_module, that was previously exported was not the
bertot
2001-04-03
*
Export a function (build_inductive) that is used in the graphical interface.
bertot
2001-04-03
*
branchement extraction (bytecode seulement)
filliatr
2001-03-30
*
amelioration de la structure des univers
barras
2001-03-28
*
amelioration de la consommation memoire de la conversion en eta-expansant
barras
2001-03-23
*
Bug MUTCASE au lieu CASE
herbelin
2001-03-22
*
entetes
filliatr
2001-03-15
*
Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisation
herbelin
2001-03-11
*
Déplacement de qualid dans Nametab, hors du noyau
herbelin
2001-03-01
*
Bug affichage coercions
herbelin
2001-02-16
*
ident au lieu de string pour le nom de base de qualid
herbelin
2001-02-16
[prev]
[next]