1) GrafiteAst.NEval => GrafiteAst.NReduce

[helm.git] / helm / software / components / grafite_parser / grafiteParser.ml

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 547e510253f64302d3f48db36e3ff366074884bc..742e538febd09a0f50b3780a319ac3d67a08c81d 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -131,6 +131,15 @@ EXTEND
     | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
     | IDENT "whd" -> `Whd ]
   ];
+  nreduction_kind: [
+    [ IDENT "nnormalize" ; delta = OPT [ IDENT "nodelta" -> () ] ->
+       let delta = match delta with None -> true | _ -> false in
+        `Normalize delta
+    (*| IDENT "unfold"; t = OPT tactic_term -> `Unfold t*)
+    | IDENT "nwhd" ; delta = OPT [ IDENT "nodelta" -> () ] ->
+       let delta = match delta with None -> true | _ -> false in
+        `Whd delta]
+  ];
   sequent_pattern_spec: [
    [ hyp_paths =
       LIST0
@@ -222,12 +231,10 @@ EXTEND
     | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
         where = pattern_spec ->
         G.NLetIn (loc,where,t,name)
+    | kind = nreduction_kind; p = pattern_spec ->
+        G.NReduce (loc, kind, p)
     | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
         G.NRewrite (loc, dir, what, where)
-    | IDENT "nwhd"; delta = OPT [ IDENT "nodelta" -> () ];
-      where = pattern_spec ->
-        let delta = match delta with None -> true | _ -> false in
-        G.NEval (loc, where, `Whd delta)
     | SYMBOL "#"; n=IDENT -> G.NIntro (loc,n)
     | SYMBOL "#"; SYMBOL "_" -> G.NIntro (loc,"_")
     | SYMBOL "*" -> G.NCase1 (loc,"_")