index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
Commit message (
Expand
)
Author
Age
*
Changement des named_context
gregoire
2005-12-02
*
amelioration de la generation des unsafeCoerce
letouzey
2005-12-01
*
evite certaines eta-expansions cavalieres
letouzey
2005-11-30
*
correctif pour que type t = M.t contienne bien son M.
letouzey
2005-11-29
*
petites corrections + contournement bug projections
barras
2005-11-18
*
commited first version of new ring
barras
2005-11-18
*
merci les warnings de 3.09 ...
letouzey
2005-11-17
*
avoids warnings about unused variables
bertot
2005-11-14
*
adds the the case VernacShow(ShowMatch _) in the pattern-matching construct,
bertot
2005-11-14
*
Nettoyage suite à la détection par défaut des variables inutilisées par o...
herbelin
2005-11-08
*
Adds tools to help in defining new general recursive functions
bertot
2005-11-07
*
Types inductifs parametriques
mohring
2005-11-02
*
changed the syntax categories of arguments of functional scheme
coq
2005-09-16
*
pas besoin de List.length pour savoir si une liste est vide
letouzey
2005-08-19
*
Sur le conseil de X.Leroy: x=[||] devient Array.length x=0
letouzey
2005-08-19
*
code cleaning. No changes as far as tested.
coq
2005-08-18
*
new congruence
corbinea
2005-08-17
*
Subtac: traitement correct des existentielles et de la récursion.
coq
2005-07-15
*
reflexive tauto
corbinea
2005-07-15
*
General recursive definitions on well founded orders support
coq
2005-07-13
*
Dp: ajout d'abstraction aux applications de fonction non premier ordre
coq
2005-06-24
*
dp: ajout des prédicats de sortes
coq
2005-06-24
*
Dp : ajoût des existentiels
coq
2005-06-15
*
dp: traitement des fixpoints
coq
2005-06-09
*
traitement des case
coq
2005-06-08
*
Correction of a bug in functional scheme. It raised with mutual
coq
2005-05-26
*
Add a guard for V7 mode, CVS compiles cleanly again :)
coq
2005-05-26
*
Added subtac contrib.
coq
2005-05-25
*
dp: ajout du prouveur Zenon
coq
2005-05-24
*
New command: "Print Ltac qualid" to print user defined tactics.
sacerdot
2005-05-20
*
Adoption du nom canonique global_of_constr pour éviter confusion avec type r...
herbelin
2005-05-20
*
added VernacBacktrack (new backtracking command dedicated to
coq
2005-05-19
*
Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...
herbelin
2005-05-17
*
Allow auto to have a parametric argument (wish #967)
herbelin
2005-05-15
*
Open Scope non Local malencontreux
herbelin
2005-05-03
*
Utilisation Z_scope
herbelin
2005-05-02
*
Gestion du forall et envoie d'axiome à la procédure
coq
2005-04-21
*
dp: traitement des definitions
coq
2005-04-07
*
Problemes de renommage regles
coq
2005-04-05
*
symboles de fonctions globaux traites
coq
2005-03-24
*
Ajout de l'axiome du but prouve par la tactique simplifi
coq
2005-03-22
*
appel de Simplify depuis Coq
coq
2005-03-18
*
tactiques prouveurs premier ordre dans contrib/dp/
coq
2005-03-16
*
nouvelles tactiques pour appeler des procedures de decision du premier ordre
coq
2005-03-16
*
Unsharing before exportation to ensure uniqueness of xml id's
herbelin
2005-03-15
*
Added 'clear - id' to clear all hypotheses except the ones dependent in the s...
herbelin
2005-03-07
*
Pas de dépendance en Omega
herbelin
2005-02-21
*
Correction de bugs: coq_false et coq_true au lieu de coq_False et coq_true
herbelin
2005-02-21
*
- changement ordre arguments interp_goal_concl pour permettre application
herbelin
2005-02-21
*
- Correction de bugs
herbelin
2005-02-21
[next]