index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
Commit message (
Expand
)
Author
Age
*
Merge from Lionel Elie Mamane's private branch:
lmamane
2007-01-10
*
Nouvelle approche pour le discharge modulaire
herbelin
2007-01-10
*
Cleaning backtracking code, optimized "Backtrack n x y" when n is
courtieu
2006-12-28
*
Addition of a "Combined Scheme" vernacular command for building the conjuncti...
msozeau
2006-12-23
*
Correction du bug #1273, deuxième version (avec des shémas d'elimination pl...
notin
2006-12-12
*
Suite ajout option -output-context
herbelin
2006-12-08
*
Ajout d'une option -output-context qui affiche le contexte en CCI pur à la
herbelin
2006-12-08
*
Fixed the -emacs option which was always On.
courtieu
2006-11-24
*
Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms de
herbelin
2006-11-21
*
The emacs-U option now does not output *any* char above 250.
courtieu
2006-11-17
*
gestion speciale du niveau 5 des ltac
barras
2006-11-02
*
Extension du polymorphisme de sorte au cas des définitions dans Type.
herbelin
2006-10-28
*
Documentation de "Set Printing Universes", "Print Universes" (anciennement
herbelin
2006-10-28
*
Ajout option Set Printing Universes et amélioration affichage des univers
herbelin
2006-10-28
*
bug #1194: normalisation evars a la sortie de focus
barras
2006-10-23
*
Add a flush after backtracking x y z and before printing subgoals.
courtieu
2006-10-23
*
Correction de la localisation des erreurs en interactif (numéro de
herbelin
2006-10-20
*
Amélioration de l'automatisation des coupures quand deux idents se suivent
herbelin
2006-10-09
*
Correction d'un bug dans l'unification: lors de l'unification d'un meta m et ...
notin
2006-10-05
*
Added a new option -emacs-U changing emacs prompt delimiters by
courtieu
2006-09-29
*
Corrections mineures
notin
2006-09-25
*
Declarative Proof Language: main commit
corbinea
2006-09-20
*
Compatibilité hyp=var dans Tactic Notation + nettoyage
herbelin
2006-09-15
*
Report de l'heuristique d'unification premier ordre flexible/rigide
herbelin
2006-09-15
*
Indentation + svnprop
notin
2006-09-12
*
Retour à un warning en cas de (co-)fixpoint pas totalement mutuel
herbelin
2006-09-09
*
Finalement, interdiction des points fixes non totalement mutuellement
herbelin
2006-09-06
*
Ajout possibilité clause "where" dans co-points fixes
herbelin
2006-09-01
*
Extension et réorganisation de l'interprétation des (co-)points fixes
herbelin
2006-09-01
*
Indentation + typo
notin
2006-09-01
*
improve the amount of information given by the Ltac tactic debugger
bertot
2006-08-28
*
Morceau de code mort
herbelin
2006-08-24
*
Modifications dans les scripts de configuration (coqtop et coqide affichent m...
notin
2006-07-28
*
Correction du bug #1116
jforest
2006-07-20
*
Branchement de 'Debug On/Off' sur le mécanisme standard d'option et donc, re...
herbelin
2006-07-05
*
Ajout d'une option -with-geoproof à la configuration et à l'exécution
notin
2006-06-09
*
Réinitialisation de token_number à chaque compilation d'un nouveau fichier ...
notin
2006-06-08
*
Réparation coqtop.ml
notin
2006-06-07
*
Changement de l'option -where: on vérifie si la variable d'environnement COQ...
notin
2006-06-07
*
The "clean integration of subtac" patch.
msozeau
2006-05-29
*
Nouvelle implantation du polymorphisme de sorte pour les familles inductives
herbelin
2006-05-23
*
Cleanning and factorizing code in funind. Spliting new_arg_principles into to...
jforest
2006-05-03
*
Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...
notin
2006-04-28
*
Standardisation nom option_app en option_map
herbelin
2006-04-27
*
Modification of emacs output: No more show script at the end of a proof.
courtieu
2006-04-27
*
Modification of emacs output: Pp.warning and al now output warning
courtieu
2006-04-27
*
Si un fixpoint a plusieurs arguments, mais un seul de type inductif,
letouzey
2006-04-14
*
Modification of "Show Intros": it now shows letins too.
courtieu
2006-04-11
*
Finalement, scopes utiles pour option 'where' (cf bug #1132)
herbelin
2006-04-07
*
Suppression du test Proof with <tac>
notin
2006-04-05
[next]