diff options
| author | clrenard | 2001-06-11 14:45:20 +0000 |
|---|---|---|
| committer | clrenard | 2001-06-11 14:45:20 +0000 |
| commit | f2d06f15a11fa4261483ac59eda33fa11f784e9a (patch) | |
| tree | 8324137172a45a71e11fa53aca527840bec19765 /parsing | |
| parent | dd0cf23cd41386cf028aa212487c35f54f149e70 (diff) | |
Reparation d'un bug d'affichage. Les let destructurants, if, et vieux Case
n'etaient pas affiches correctement lors du Save si on les avait donne en
argument de tactique. Avec Bruno, nous avons simplifie l'ast en remplacant
les MLCASE NOREC et autres CASE NOREC par des choses plus simples.
Il y a maintenant un noeud LET, un IF, un CASE et un MATCH qui sont a peu pres
semblables mais qui permettent de se souvenir quoi afficher.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1781 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/astterm.ml | 8 | ||||
| -rw-r--r-- | parsing/g_constr.ml4 | 23 |
2 files changed, 15 insertions, 16 deletions
diff --git a/parsing/astterm.ml b/parsing/astterm.ml index 85bd1a3e5f..45b6b6ae97 100644 --- a/parsing/astterm.ml +++ b/parsing/astterm.ml @@ -467,13 +467,13 @@ let ast_to_rawconstr sigma env allow_soapp lvar = List.map (dbrec env) tms, List.map (ast_to_eqn (List.length tms) env) eqns) - | Node(loc,"CASE",Str(_,isrectag)::p::c::cl) -> + | Node(loc,(("CASE"|"IF"|"LET"|"MATCH")as tag), p::c::cl) -> let po = match p with | Str(_,"SYNTH") -> None | _ -> Some(dbrec env p) in - let isrec = match isrectag with - | "REC" -> true | "NOREC" -> false - | _ -> anomaly "ast_to: wrong REC tag in CASE" in + let isrec = match tag with + | "MATCH" -> true | ("LET"|"CASE"|"IF") -> false + | _ -> anomaly "ast_to: wrong tag in old case expression" in ROldCase (loc,isrec,po,dbrec env c, Array.of_list (List.map (dbrec env) cl)) diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index ff4a0a7580..56779d71f0 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -92,39 +92,38 @@ GEXTEND Gram [ [ "<"; ":"; IDENT "ast"; ":"; "<"; c = raw_constr; ">>" -> c | "<"; l1 = lconstr; ">"; IDENT "Match"; c = constr; "with"; cl = ne_constr_list; "end" -> - <:ast< (CASE "REC" $l1 $c ($LIST $cl)) >> + <:ast< (MATCH $l1 $c ($LIST $cl)) >> | "<"; l1 = lconstr; ">"; IDENT "Match"; c = constr; "with"; "end" -> - <:ast< (CASE "REC" $l1 $c) >> + <:ast< (MATCH $l1 $c) >> | "<"; l1 = lconstr; ">"; IDENT "Case"; c = constr; "of"; cl = ne_constr_list; "end" -> - <:ast< (CASE "NOREC" $l1 $c ($LIST $cl)) >> + <:ast< (CASE $l1 $c ($LIST $cl)) >> | "<"; l1 = lconstr; ">"; IDENT "Case"; c = constr; "of"; "end" -> - <:ast< (CASE "NOREC" $l1 $c) >> + <:ast< (CASE $l1 $c) >> | IDENT "Case"; c = constr; "of"; cl = ne_constr_list; "end" -> - <:ast< (CASE "NOREC" "SYNTH" $c ($LIST $cl)) >> + <:ast< (CASE "SYNTH" $c ($LIST $cl)) >> | IDENT "Case"; c = constr; "of"; "end" -> - <:ast< (CASE "NOREC" "SYNTH" $c) >> + <:ast< (CASE "SYNTH" $c) >> | IDENT "Match"; c = constr; "with"; cl = ne_constr_list; "end" -> - <:ast< (CASE "REC" "SYNTH" $c ($LIST $cl)) >> + <:ast< (MATCH "SYNTH" $c ($LIST $cl)) >> | IDENT "let"; "("; b = ne_ident_comma_list; ")"; "="; c = constr; "in"; c1 = constr -> - <:ast< (CASE "NOREC" "SYNTH" $c (LAMBDALIST (ISEVAR) - ($SLAM $b $c1))) >> + <:ast< (LET "SYNTH" $c (LAMBDALIST (ISEVAR) ($SLAM $b $c1))) >> | IDENT "let"; id1 = IDENT ; "="; c = constr; "in"; c1 = constr -> <:ast< (LETIN $c [$id1]$c1) >> | IDENT "if"; c1 = constr; IDENT "then"; c2 = constr; IDENT "else"; c3 = constr -> - <:ast< ( CASE "NOREC" "SYNTH" $c1 $c2 $c3) >> + <:ast< ( IF "SYNTH" $c1 $c2 $c3) >> (* EN ATTENTE DE REMPLACER CE QUI EST DANS Program.v ... *) | "<"; l1 = lconstr; ">"; IDENT "let"; "("; b = ne_ident_comma_list; ")"; "="; c = constr; "in"; c1 = constr -> - <:ast< (CASE "NOREC" $l1 $c (LAMBDALIST (ISEVAR) ($SLAM $b $c1))) >> + <:ast< (LET $l1 $c (LAMBDALIST (ISEVAR) ($SLAM $b $c1))) >> | "<"; l1 = lconstr; ">"; IDENT "if"; c1 = constr; IDENT "then"; c2 = constr; IDENT "else"; c3 = constr -> - <:ast< (CASE "NOREC" $l1 $c1 $c2 $c3) >> + <:ast< (IF $l1 $c1 $c2 $c3) >> | c = constr0 -> c ] ] ; constr2: (* ~ will be here *) |