index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
translate
Commit message (
Expand
)
Author
Age
*
Restructuration des points d'entrée de Pretyping et Constrintern
herbelin
2005-12-21
*
Changement des named_context
gregoire
2005-12-02
*
Nettoyage suite à la détection par défaut des variables inutilisées par o...
herbelin
2005-11-08
*
- debugging og "Show Intros": no line breaking + fresh ids
coq
2005-11-08
*
New command: "Print Ltac qualid" to print user defined tactics.
sacerdot
2005-05-20
*
Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...
herbelin
2005-05-17
*
Globalisation des Tactic Notation
herbelin
2005-05-15
*
Allow auto to have a parametric argument (wish #967)
herbelin
2005-05-15
*
Implementation of a new backtracking system, that allow to go back
coq
2005-04-20
*
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 constructeur External pour appel outil externe à Coq
herbelin
2005-02-04
*
Ajout constructeur External pour appel outil externe à Coq
herbelin
2005-02-04
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-21
*
Ajout de la syntaxe du reset label: "BackTo n".
coq
2005-01-14
*
Construct "T with (Definition|Module) id := c" generalized to
sacerdot
2005-01-13
*
- Module/Declare Module syntax made more uniform:
sacerdot
2005-01-06
*
Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...
herbelin
2005-01-02
*
ExtraRedExpr maintenant sans argument: pas très souple mais au moins convien...
herbelin
2004-12-29
*
Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...
herbelin
2004-12-24
*
pp of nested fixpoints (dangling with/for)
barras
2004-12-01
*
Export pr_intro_pattern
herbelin
2004-11-30
*
New command "Print Rewrite HindDb dbname".
sacerdot
2004-11-17
*
Ajout 'Locate Module'
herbelin
2004-11-17
*
Affichage des univers
herbelin
2004-11-04
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
Mise en conformité de la syntaxe de Theorem/Lemma avec la doc: les lieurs so...
herbelin
2004-10-12
*
'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...
herbelin
2004-10-11
*
restructuration des printers: proofs passe avant parsing
barras
2004-09-17
*
Ajout de or-pattern pour le match-with v8
herbelin
2004-09-09
*
"Print Setoids" command added.
sacerdot
2004-07-23
*
Abstraction vis à vis du type loc pour compatibilité ocaml 3.08
herbelin
2004-07-16
*
Nouvelle en-tête
herbelin
2004-07-16
*
moved instantiate binding to extratactics
corbinea
2004-06-29
*
more evar stuff
corbinea
2004-06-28
*
Plus de robustesse en traduisant les 'Repeat Induction' et les 'Do n Induction'
herbelin
2004-06-02
*
pb facto des Fixpoint + erreur avec -dump-glob et Load
barras
2004-04-17
*
Chgt role 2eme argument AList et implantation affichage motifs recursifs de n...
herbelin
2004-04-08
*
code mort
herbelin
2004-03-24
*
Traduction ad hoc pour Hint Rewrite in using
herbelin
2004-03-18
*
Hack pour traduction des changements non uniformes de syntaxe des TACTIC et V...
herbelin
2004-03-17
*
Hack pour traduction des changements non uniformes de syntaxe des TACTIC et V...
herbelin
2004-03-17
*
Mise en place de motifs récursifs dans Notation; quelques simplifications au...
herbelin
2004-03-17
*
Bug inversion abstract_constr_expr et prod_constr_expr
herbelin
2004-03-12
*
modif des fixpoints pour que si on donne une notation au produit, les pts fix...
barras
2004-03-05
*
Retablissement pour le traducteur d'une copie de pr_intro_pattern base sur la...
herbelin
2004-03-05
*
Plus de noms d'entrees de grammaires qualifies dans 'Tactic Notation'
herbelin
2004-03-03
*
Changement de natural en int_or_var pour 'do' et 'fail' pour paramétrisation...
herbelin
2004-03-02
*
Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...
herbelin
2004-03-02
[next]