summaryrefslogtreecommitdiff
path: root/proofs/redexpr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/redexpr.ml')
-rw-r--r--proofs/redexpr.ml26
1 files changed, 14 insertions, 12 deletions
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 7290a92f..0430a239 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -1,20 +1,18 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: redexpr.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Pp
open Util
open Names
open Term
open Declarations
open Libnames
-open Rawterm
+open Glob_term
open Pattern
open Reductionops
open Tacred
@@ -40,12 +38,13 @@ let set_strategy_one ref l =
Csymtable.set_opaque_const sp
| ConstKey sp, _ ->
let cb = Global.lookup_constant sp in
- if cb.const_body <> None & cb.const_opaque then
- errorlabstrm "set_transparent_const"
- (str "Cannot make" ++ spc () ++
- Nametab.pr_global_env Idset.empty (ConstRef sp) ++
- spc () ++ str "transparent because it was declared opaque.");
- Csymtable.set_transparent_const sp
+ (match cb.const_body with
+ | OpaqueDef _ ->
+ errorlabstrm "set_transparent_const"
+ (str "Cannot make" ++ spc () ++
+ Nametab.pr_global_env Idset.empty (ConstRef sp) ++
+ spc () ++ str "transparent because it was declared opaque.");
+ | _ -> Csymtable.set_transparent_const sp)
| _ -> ()
let cache_strategy (_,str) =
@@ -87,7 +86,10 @@ let discharge_strategy (_,(local,obj)) =
if local then None else
map_strategy disch_ref obj
-let (inStrategy,outStrategy) =
+type strategy_obj =
+ bool * (Conv_oracle.level * evaluable_global_reference list) list
+
+let inStrategy : strategy_obj -> obj =
declare_object {(default_object "STRATEGY") with
cache_function = (fun (_,obj) -> cache_strategy obj);
load_function = (fun _ (_,obj) -> cache_strategy obj);
@@ -213,7 +215,7 @@ let subst_red_expr subs e =
(Pattern.subst_pattern subs)
e
-let (inReduction,_) =
+let inReduction : bool * string * red_expr -> obj =
declare_object
{(default_object "REDUCTION") with
cache_function = (fun (_,(_,s,e)) -> decl_red_expr s e);