index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
/
interface
Commit message (
Expand
)
Author
Age
*
Ajout construction If primitive dans constr_expr et rawconstr
herbelin
2003-09-09
*
Mise en place possibilité de définitions locales dans les paramètres des r...
herbelin
2003-09-06
*
Mise en place possibilité de définitions locales dans les paramètres des i...
herbelin
2003-09-06
*
Nouvelle mouture du traducteur v7->v8
herbelin
2003-08-11
*
Ajout 'Symmetry in Hyp'
herbelin
2003-06-19
*
Ajout option Local à Hint, Hints et HintDestruct
herbelin
2003-06-14
*
Utilisation de intro_pattern dans NewDestruct/NewInduction
herbelin
2003-06-13
*
Ajout notation c.(f) en v8 pour les projections de Record
herbelin
2003-06-10
*
Suppression définitive de lmatch et or_metanum dans tacinterp
herbelin
2003-05-21
*
MAJ
herbelin
2003-05-21
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
Localisation erreurs TacAlias; Globalisation moins tolérante dans les
herbelin
2003-04-28
*
Ajout "at next level" dans Notation
herbelin
2003-04-17
*
Ajout option 'Local' à Infix et Notation
herbelin
2003-04-11
*
Réorganisation de Impargs + mise en place d'une infrastructure
herbelin
2003-04-09
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07
*
Ajout d'un message à FailTac
herbelin
2003-03-31
*
factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )
corbinea
2003-03-31
*
*** empty log message ***
barras
2003-03-12
*
Remove a TODO in the translation of generic arguments:
bertot
2003-03-10
*
Make sure that identifiers are parsed as qualified identifier and that
bertot
2003-03-06
*
Ajout du traducteur
desmettr
2003-02-05
*
Added a clause for VernacDefineModule, but with an error as result.
bertot
2003-02-03
*
all tactics should be covered now: remains
bertot
2003-01-26
*
Add translations for many tactics but a dozen are still remaining
bertot
2003-01-25
*
Inspect does not work for pcoq and there is no simple fix because inspect
bertot
2003-01-24
*
The data constructed when detecting an error in a list of commands must
bertot
2003-01-24
*
Corrects the way conjunctions, existential quantifications, and arrows are
bertot
2003-01-24
*
Make sure proof by pointing works.
bertot
2003-01-23
*
Make proof by pointing work for the new notations of existential quantification.
bertot
2003-01-23
*
removes all references to ctast.ml the Makefile has been updated accordingly.
bertot
2003-01-22
*
Make sure pcoq will also display hypotheses with a value.
bertot
2003-01-21
*
Add a few operators in the new version of xlate.ml and make sure
bertot
2003-01-21
*
Restructuration interpréteur de tactique: plus d'évaluation partielle à la...
herbelin
2003-01-19
*
Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à un...
herbelin
2003-01-15
*
SearchAbout
filliatr
2003-01-06
*
Légère amélioration des messages d'erreur des with-bindings et des Rewrite
herbelin
2002-12-21
*
simplification de solve_subgoal: n'utilise plus frontier
barras
2002-12-19
*
Ajout "Locate Notation"
herbelin
2002-12-15
*
Ajout du vernac Proof with
gregoire
2002-12-12
*
Ajout options -v7 et -v8, et commandes V7only et V8only
herbelin
2002-12-10
*
Ajoute le bon traitement pour Ring, Locate, Comments
bertot
2002-12-09
*
Take notations into account: numbers and the CNotation operator.
bertot
2002-12-09
*
Ajout Simpl et Change sur des sous-termes
herbelin
2002-12-09
*
Modification Require From
mohring
2002-12-04
*
la table PARAMETER n'existe plus (mergé dans la table CONSTANT)
letouzey
2002-12-03
*
Etape intermédiaire d'adaptation de la connexion à pcoq aux nouvelles
bertot
2002-12-03
*
Raffinement syntaxe Infix
herbelin
2002-11-29
*
Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...
herbelin
2002-11-24
*
Complétion du commit précédent
herbelin
2002-11-16
[next]