Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

54 lines (35 sloc) 1.56 kb
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)
Jump to Line
Something went wrong with that request. Please try again.