Distribution: - faire une passe sur les options de coqtop et coqc Langage: - Propager les contraintes arrière dans Cases (cf example doc/Cases.tex) Environnement: - Porter SearchIsos Noyau: Vernac: - Print / Print Proof en fait identiques ; Print ne devrait pas afficher les constantes opaques (devrait afficher qqchose comme ) Grammaires: - revoir numarg/pure_numarg dans g_tactic.ml4 (regles a factoriser) Doc: - documenter AutoRewrite - 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 - une passe sur le chapitre extensions de syntaxe - documenter le langage de tactique et Field - revoir le chapitre sur les tactiques utilisateur - faut-il mieux spécifier la sémantique de Simpl (??) - documenter @Definition and co - Suggestions de la formation Dans le Intros pattern on pourrait interpreter les _ comme des hypotheses sur lesquelles on ferait Clear immediatement -> FAIT, semble-t'il