diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-03-14 09:45:23 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-03-14 09:45:23 +0000 |
commit | f30bd39de0f634b8c4b7745e8781cea13109cae1 (patch) | |
tree | f787d6fec03198cdfae8fb13491b2302d3168acc /TODO | |
parent | 49dfb05f28436c25be64f5ca381c9ee3b6dee8f5 (diff) |
MAJ
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1461 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'TODO')
-rw-r--r-- | TODO | 8 |
1 files changed, 0 insertions, 8 deletions
@@ -7,7 +7,6 @@ Distribution: Environnement: - Porter SearchIsos -- Interdire de faire 2 fois la même définition avec le même nom absolu FAIT Tactiques: @@ -15,19 +14,12 @@ Tactiques: Noyau: -- Gérer les let in dans la condition de garde, exemple: - Fixpoint F [n:nat]:nat:= Cases n of O => O | (S n0) => - Cases n0 of O => (S O) | (S n1) => [n2:=(S n1)](S (F n2)) end - - Vernac: -- Imprimer les paths avec "." FAIT - Pb noms cachés (utilisation de noms absolus ?) Grammaires: -- pb avec les extensions constr (cf Zsyntax et Cases x of `0` => ...) - revoir numarg/pure_numarg dans g_tactic.ml4 (regles a factoriser) Doc: |