index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
/
interface
/
xlate.ml
Commit message (
Expand
)
Author
Age
*
Extension de fresh (suite)
herbelin
2006-10-24
*
Une passe sur l'injection et la discrimination...
herbelin
2006-10-01
*
mise a jour du nouveau ring et ajout du nouveau field, avant renommages
barras
2006-09-26
*
Declarative Proof Language: main commit
corbinea
2006-09-20
*
Ajout possibilité clause "where" dans co-points fixes
herbelin
2006-09-01
*
making otags working
jforest
2006-08-22
*
+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and no
jforest
2006-08-22
*
Suite remplacement VernacDebug par VernacSetOption
herbelin
2006-07-06
*
Extension des motifs disjonctifs au cas de disjonction de motifs multiples
herbelin
2006-07-03
*
Suite passage ident -> hyp dans syntaxe de 'replace with in'
herbelin
2006-06-23
*
Changement du type d'argument 'TacticArgType X' en un type
herbelin
2006-06-08
*
Détection bug rawwit suitecorrection trou de typage create_arg
herbelin
2006-06-08
*
Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...
herbelin
2006-05-30
*
Extension syntaxique de rewrite in: au lieu de pouvoir faire
letouzey
2006-05-02
*
Standardisation nom option_app en option_map
herbelin
2006-04-27
*
Si un fixpoint a plusieurs arguments, mais un seul de type inductif,
letouzey
2006-04-14
*
+ destruct now works as induction on multiple arguments :
jforest
2006-03-21
*
Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.
msozeau
2006-03-13
*
induction now admits multiple induction arguments. The principle must
coq
2006-02-10
*
Réorganisation de la structure interne des types de déclarations (decl_kinds)
herbelin
2006-01-28
*
Ajout option 'using lemmas' à auto/trivial/eauto
herbelin
2006-01-28
*
Suppression code pour hints nommés à la V7 (voire à la V6...)
herbelin
2006-01-28
*
Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et f...
herbelin
2006-01-21
*
Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq
herbelin
2006-01-16
*
- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses
herbelin
2006-01-16
*
Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux de...
herbelin
2005-12-30
*
Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...
herbelin
2005-12-26
*
Achèvement suppression traducteur dans contrib/interface
herbelin
2005-12-26
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...
herbelin
2005-12-26
*
Simplifification de vernac_expr li l'abandon du traducteur
herbelin
2005-12-23
*
Changement des named_context
gregoire
2005-12-02
*
adds the the case VernacShow(ShowMatch _) in the pattern-matching construct,
bertot
2005-11-14
*
New command: "Print Ltac qualid" to print user defined tactics.
sacerdot
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
*
Added 'clear - id' to clear all hypotheses except the ones dependent in the s...
herbelin
2005-03-07
*
Renaming Print Canonical Structure into Print Canonical Projections
herbelin
2005-02-18
*
Ajout Print Canonical Structures
herbelin
2005-02-12
*
Ajout cas VernacBackTo
herbelin
2005-01-26
*
Construct "T with (Definition|Module) id := c" generalized to
sacerdot
2005-01-13
*
- Module/Declare Module syntax made more uniform:
sacerdot
2005-01-06
*
Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...
herbelin
2004-12-24
*
Restauration type casted_open_constr pour tactique refine car l'unification n...
herbelin
2004-12-09
*
Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti...
herbelin
2004-12-06
*
Correction 1.138 appliquée à tort à la branche principale au lieu de V8-0b...
herbelin
2004-11-29
*
Commit précédent erroné; retour version précédente
herbelin
2004-11-29
*
MAJ vis à vis de extratactics
herbelin
2004-11-28
*
Locate Module
herbelin
2004-11-17
*
New command "Print Rewrite HindDb dbname".
sacerdot
2004-11-17
[next]