diff options
Diffstat (limited to 'proofs/redexpr.ml')
| -rw-r--r-- | proofs/redexpr.ml | 26 |
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); |