From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 28 Apr 2006 14:59:16 +0000
Subject: Imported Upstream version 8.0pl3+8.1alpha

---
 pretyping/tacred.mli | 24 ++++++++++--------------
 1 file changed, 10 insertions(+), 14 deletions(-)

(limited to 'pretyping/tacred.mli')

diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 7998a8fd..a5468435 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tacred.mli,v 1.21.2.2 2005/01/21 16:42:37 herbelin Exp $ i*)
+(*i $Id: tacred.mli 8003 2006-02-07 22:11:50Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -18,15 +18,23 @@ open Closure
 open Rawterm
 (*i*)
 
+type reduction_tactic_error = 
+    InvalidAbstraction of env * constr * (env * Type_errors.type_error)
+
+exception ReductionTacticError of reduction_tactic_error
+
 (*s Reduction functions associated to tactics. \label{tacred} *)
 
 val is_evaluable : env -> evaluable_global_reference -> bool
 
 exception Redelimination
 
-(* Red (raise Redelimination if nothing reducible) *)
+(* Red (raise user error if nothing reducible) *)
 val red_product : reduction_function
 
+(* Red (raise Redelimination if nothing reducible) *)
+val try_red_product : reduction_function
+
 (* Hnf *)
 val hnf_constr :  reduction_function
 
@@ -69,17 +77,5 @@ val reduce_to_quantified_ref :
 val reduce_to_atomic_ref :
   env ->  evar_map -> Libnames.global_reference -> types -> types
 
-type red_expr = (constr, evaluable_global_reference) red_expr_gen
-
 val contextually : bool -> constr occurrences -> reduction_function
   -> reduction_function
-val reduction_of_redexp : red_expr -> reduction_function
-
-val declare_red_expr : string -> reduction_function -> unit
-
-(* Opaque and Transparent commands. *)
-val set_opaque_const      : constant -> unit
-val set_transparent_const : constant -> unit
-
-val set_opaque_var      : identifier -> unit
-val set_transparent_var : identifier -> unit
-- 
cgit v1.2.3