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
*
Adding a syntax for "n-ary" rewrite:
letouzey
2007-07-06
*
sequel to commit 9952: forgot to adapt xlate to the new n-ary rename
letouzey
2007-07-06
*
New intro pattern "@A", which generates a fresh name based on A.
glondu
2007-07-06
*
killing some more non-exhaustive patterns
letouzey
2007-06-26
*
Modification of VernacScheme to handle a new scheme: Equality (equality in
vsiles
2007-05-25
*
- Propagation des evars non résolues vers les with_bindings; permet par exemple
herbelin
2007-05-20
*
Nouveaux changements autour des implicites (notamment suite à
herbelin
2007-05-06
*
Ajout possibilité d'options à trois mots.
herbelin
2007-04-29
*
Ajout de la possibilité de faire référence dans certains cas à un nom
herbelin
2007-04-28
*
Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.
herbelin
2007-04-28
*
New keyword "Inline" for Parameters and Axioms for automatic
soubiran
2007-04-25
*
Export de simplest_eapply, utilisé dans la contrib interface
notin
2007-04-16
*
Extension to the general sequence operator (tactical). Now in addition to ...
emakarov
2007-04-02
*
Forgot to update to new cast
msozeau
2007-03-19
*
Achèvement commit 9677 (suppression résidu v7 dans PrintGrammar)
herbelin
2007-02-24
*
Coqdoc patch for Program, fix xlate.ml warning and little subtac fixes.
msozeau
2007-01-29
*
Merge from Lionel Elie Mamane's private branch:
lmamane
2007-01-10
*
Nouvelle approche pour le discharge modulaire
herbelin
2007-01-10
*
Changement dans le kernel :
bgregoir
2006-12-11
*
Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms de
herbelin
2006-11-21
*
Extension du polymorphisme de sorte au cas des définitions dans Type.
herbelin
2006-10-28
*
Extension de fresh (suite)
herbelin
2006-10-24
*
affichage des ... dans les scripts
barras
2006-10-16
*
Notations:
herbelin
2006-10-09
*
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
*
Suite commit 9110 (uniformisation position notation dans les blocs inductifs)
herbelin
2006-09-01
*
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
*
Nouvelle implantation du polymorphisme de sorte pour les familles inductives
herbelin
2006-05-23
*
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
*
Made pretyping a functor over a coercion implementation. Pretyping.Default us...
msozeau
2006-03-22
*
+ destruct now works as induction on multiple arguments :
jforest
2006-03-21
*
Modification des propriétés (svn:executable)
notin
2006-03-17
*
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
*
Suppression de la dépendance en Map.fold de ocaml dont la sémantique a
herbelin
2006-01-24
[next]