Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

file 51 lines (35 sloc) 1.56 kb
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51
Langage:

Distribution:

Environnement:

- Porter SearchIsos

Noyau:

Tactic:

- Que contradiction raisonne a isomorphisme pres de False

Vernac:

- Print / Print Proof en fait identiques ; Print ne devrait pas afficher
  les constantes opaques (devrait afficher qqchose comme <opaque>)

Theories:

- Rendre transparent tous les theoremes prouvant {A}+{B}
- Faire demarrer PolyList.nth a` l'indice 0
  Renommer l'actuel nth en nth1 ??

Doc:

- Mettre à jour les messages d'erreurs de Discriminate/Simplify_eq/Injection
- Documenter le filtrage sur les types inductifs avec let-ins (dont la
  compatibilite V6)

- Ajouter let dans les règles du CIC
  -> FAIT, mais reste a documenter le let dans les inductifs
  et les champs manifestes dans les Record
- revoir le chapitre sur les tactiques utilisateur
- faut-il mieux spécifier la sémantique de Simpl (??)

- Préciser la clarification syntaxique de IntroPattern
- preciser que Goal vient en dernier dans une clause pattern list et
  qu'il doit apparaitre si il y a un "in"

- Omega Time debranche mais Omega System et Omega Action remarchent ?
- Ajout "Replace in" (mais TODO)
- Syntaxe Conditional tac Rewrite marche, à documenter
- Documenter Dependent Rewrite et CutRewrite ?
- Ajouter les motifs sous-termes de ltac

- ajouter doc de GenFixpoint (mais avant: changer syntaxe) (J. Forest ou Pierre C.)
- mettre à jour la doc de induction (arguments multiples) (Pierre C.)
- mettre à jour la doc de functional induction/scheme (J. Forest ou Pierre C.)
--> mettre à jour le CHANGES (vers la ligne 72)
Something went wrong with that request. Please try again.