From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 proofs/redexpr.mli | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

(limited to 'proofs/redexpr.mli')

diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index d72ff182..03d97ce3 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -6,24 +6,31 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: redexpr.mli 11094 2008-06-10 19:35:23Z herbelin $ i*)
+(*i $Id$ i*)
 
 open Names
 open Term
 open Closure
+open Pattern
 open Rawterm
 open Reductionops
 open Termops
 
-
-type red_expr = (constr, evaluable_global_reference) red_expr_gen
+type red_expr =
+    (constr, evaluable_global_reference, constr_pattern) red_expr_gen
 
 val out_with_occurrences : 'a with_occurrences -> occurrences * 'a
 
 val reduction_of_red_expr : red_expr -> reduction_function * cast_kind
 (* [true] if we should use the vm to verify the reduction *)
 
-val declare_red_expr : string -> reduction_function -> unit
+(* Adding a custom reduction (function to be use at the ML level)
+   NB: the effect is permanent. *)
+val declare_reduction : string -> reduction_function -> unit
+
+(* Adding a custom reduction (function to be called a vernac command).
+   The boolean flag is the locality. *)
+val declare_red_expr : bool -> string -> red_expr -> unit
 
 (* Opaque and Transparent commands. *)
 
-- 
cgit v1.2.3