From 5ae4b17ab09b81ba133f13e383106a4f9620d5d4 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 28 Jan 2010 17:27:46 +0000
Subject: New command Declare Reduction <id> := <conv_expr>.

 Let's avoid writing huge "Eval ... in ..." lines :-)
 Will be used in particular soon in NMake for defining function via
  Definition ... := Eval ... in ...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12699 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/setoid_ring/newring.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index e85c12c591..cd9137fd08 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -878,7 +878,7 @@ let _ = add_map "field_cond"
 (*                       (function -1|8|10->Eval|9->Rec|_->Prot)]);;*)
 
 
-let _ = Redexpr.declare_red_expr "simpl_field_expr"
+let _ = Redexpr.declare_reduction "simpl_field_expr"
   (protect_red "field")
 
 
-- 
cgit v1.2.3