From a6dedd0d1184ae67c6ff48323f2df17dc1d42ef2 Mon Sep 17 00:00:00 2001
From: Pierre Boutillier
Date: Tue, 4 Feb 2014 15:19:25 +0100
Subject: Simpl_behaviour becomes Reductionops.ReductionBehaviour

syntax mentionning simpl remains
---
 parsing/g_vernac.ml4 | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index d5ff2538c4..371dae6c81 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -629,10 +629,10 @@ GEXTEND Gram
            error "All arguments lists must have the same length";
          let err_incompat x y =
            error ("Options \""^x^"\" and \""^y^"\" are incompatible") in
-         if nargs > 0 && List.mem `SimplNeverUnfold mods then
+         if nargs > 0 && List.mem `ReductionNeverUnfold mods then
            err_incompat "simpl never" "/";
-         if List.mem `SimplNeverUnfold mods &&
-            List.mem `SimplDontExposeCase mods then
+         if List.mem `ReductionNeverUnfold mods &&
+            List.mem `ReductionDontExposeCase mods then
            err_incompat "simpl never" "simpl nomatch";
          VernacArguments (qid, impl, nargs, mods)
 
@@ -665,8 +665,8 @@ GEXTEND Gram
 	     VernacGeneralizable gen ] ]
   ;
   arguments_modifier:
-    [ [ IDENT "simpl"; IDENT "nomatch" -> [`SimplDontExposeCase]
-      | IDENT "simpl"; IDENT "never" -> [`SimplNeverUnfold]
+    [ [ IDENT "simpl"; IDENT "nomatch" -> [`ReductionDontExposeCase]
+      | IDENT "simpl"; IDENT "never" -> [`ReductionNeverUnfold]
       | IDENT "default"; IDENT "implicits" -> [`DefaultImplicits]
       | IDENT "clear"; IDENT "implicits" -> [`ClearImplicits]
       | IDENT "clear"; IDENT "scopes" -> [`ClearScopes]
-- 
cgit v1.2.3