From cf95f2a791c263c7aaa3b488d1b09eaafc29be2b Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 27 Jun 2016 16:30:32 +0200 Subject: closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module) For the moment, there is a Closure module in compiler-libs/ocamloptcomp.cm(x)a --- plugins/cc/cctac.ml | 8 ++++---- plugins/decl_mode/decl_interp.ml | 4 ++-- plugins/decl_mode/decl_proof_instr.ml | 8 ++++---- plugins/firstorder/formula.ml | 10 +++++----- plugins/firstorder/formula.mli | 2 +- plugins/firstorder/ground.ml | 4 ++-- plugins/funind/functional_principles_proofs.ml | 6 +++--- plugins/funind/functional_principles_types.ml | 2 +- plugins/funind/invfun.ml | 2 +- plugins/funind/recdef.ml | 6 +++--- plugins/rtauto/refl_tauto.ml | 8 ++++---- plugins/setoid_ring/newring.ml | 2 +- 12 files changed, 31 insertions(+), 31 deletions(-) (limited to 'plugins') diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 6f6122d50..aff60eaa4 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -38,12 +38,12 @@ let _True = reference ["Init";"Logic"] "True" let _I = reference ["Init";"Logic"] "I" let whd env= - let infos=Closure.create_clos_infos Closure.betaiotazeta env in - (fun t -> Closure.whd_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos CClosure.betaiotazeta env in + (fun t -> CClosure.whd_val infos (CClosure.inject t)) let whd_delta env= - let infos=Closure.create_clos_infos Closure.all env in - (fun t -> Closure.whd_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos CClosure.all env in + (fun t -> CClosure.whd_val infos (CClosure.inject t)) (* decompose member of equality in an applicative format *) diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 10c09c8d6..a862423e9 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -153,8 +153,8 @@ let interp_constr check_sort env sigma c = fst (understand env sigma (fst c)) let special_whd env = - let infos=Closure.create_clos_infos Closure.all env in - (fun t -> Closure.whd_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos CClosure.all env in + (fun t -> CClosure.whd_val infos (CClosure.inject t)) let _eq = lazy (Universes.constr_of_global (Coqlib.glob_eq)) diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 5ed426c1d..97c9d5f4a 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -84,12 +84,12 @@ let tcl_erase_info gls = tcl_change_info_gen info_gen gls let special_whd gl= - let infos=Closure.create_clos_infos Closure.all (pf_env gl) in - (fun t -> Closure.whd_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos CClosure.all (pf_env gl) in + (fun t -> CClosure.whd_val infos (CClosure.inject t)) let special_nf gl= - let infos=Closure.create_clos_infos Closure.betaiotazeta (pf_env gl) in - (fun t -> Closure.norm_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos CClosure.betaiotazeta (pf_env gl) in + (fun t -> CClosure.norm_val infos (CClosure.inject t)) let is_good_inductive env ind = let mib,oib = Inductive.lookup_mind_specif env ind in diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 2ed436c6b..58744b575 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -19,7 +19,7 @@ open Context.Rel.Declaration let qflag=ref true -let red_flags=ref Closure.betaiotazeta +let red_flags=ref CClosure.betaiotazeta let (=?) f g i1 i2 j1 j2= let c=f i1 i2 in @@ -59,12 +59,12 @@ let ind_hyps nevar ind largs gls= Array.map myhyps types let special_nf gl= - let infos=Closure.create_clos_infos !red_flags (pf_env gl) in - (fun t -> Closure.norm_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos !red_flags (pf_env gl) in + (fun t -> CClosure.norm_val infos (CClosure.inject t)) let special_whd gl= - let infos=Closure.create_clos_infos !red_flags (pf_env gl) in - (fun t -> Closure.whd_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos !red_flags (pf_env gl) in + (fun t -> CClosure.whd_val infos (CClosure.inject t)) type kind_of_formula= Arrow of constr*constr diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli index 0f70d3ea0..5db8ff59a 100644 --- a/plugins/firstorder/formula.mli +++ b/plugins/firstorder/formula.mli @@ -11,7 +11,7 @@ open Globnames val qflag : bool ref -val red_flags: Closure.RedFlags.reds ref +val red_flags: CClosure.RedFlags.reds ref val (=?) : ('a -> 'a -> int) -> ('b -> 'b -> int) -> 'a -> 'a -> 'b -> 'b -> int diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index d7da85b4f..628af4e71 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -24,8 +24,8 @@ let update_flags ()= in List.iter f (Classops.coercions ()); red_flags:= - Closure.RedFlags.red_add_transparent - Closure.betaiotazeta + CClosure.RedFlags.red_add_transparent + CClosure.betaiotazeta (Names.Id.Pred.full,Names.Cpred.complement !predref) let ground_tac solver startseq gl= diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 13bc81019..215c850b6 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -223,8 +223,8 @@ let isAppConstruct ?(env=Global.env ()) t = let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *) let clos_norm_flags flgs env sigma t = - Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in - clos_norm_flags Closure.betaiotazeta Environ.empty_env Evd.empty + CClosure.norm_val (CClosure.create_clos_infos flgs env) (CClosure.inject (Reductionops.nf_evar sigma t)) in + clos_norm_flags CClosure.betaiotazeta Environ.empty_env Evd.empty @@ -1085,7 +1085,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam match Global.body_of_constant const with | Some body -> Tacred.cbv_norm_flags - (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) + (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) (Global.env ()) (Evd.empty) body diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 18ef53276..5e72b8672 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -400,7 +400,7 @@ let get_funs_constant mp dp = match Global.body_of_constant const with | Some body -> let body = Tacred.cbv_norm_flags - (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) + (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) (Global.env ()) (Evd.from_env (Global.env ())) body diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index ad5d077d6..e0c60d6d5 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -90,7 +90,7 @@ let observe_tac s tac g = (* [nf_zeta] $\zeta$-normalization of a term *) let nf_zeta = - Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) + Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) Environ.empty_env Evd.empty diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 5562100e9..027fe5677 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -92,15 +92,15 @@ let const_of_ref = function let nf_zeta env = - Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) + Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) env Evd.empty let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *) let clos_norm_flags flgs env sigma t = - Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in - clos_norm_flags Closure.betaiotazeta Environ.empty_env Evd.empty + CClosure.norm_val (CClosure.create_clos_infos flgs env) (CClosure.inject (Reductionops.nf_evar sigma t)) in + clos_norm_flags CClosure.betaiotazeta Environ.empty_env Evd.empty diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 7367a47ea..4ed907951 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -67,12 +67,12 @@ let l_D_Or = lazy (constant "D_Or") let special_whd gl= - let infos=Closure.create_clos_infos Closure.all (pf_env gl) in - (fun t -> Closure.whd_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos CClosure.all (pf_env gl) in + (fun t -> CClosure.whd_val infos (CClosure.inject t)) let special_nf gl= - let infos=Closure.create_clos_infos Closure.betaiotazeta (pf_env gl) in - (fun t -> Closure.norm_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos CClosure.betaiotazeta (pf_env gl) in + (fun t -> CClosure.norm_val infos (CClosure.inject t)) type atom_env= {mutable next:int; diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index c08813f6e..90f5f8e63 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -12,7 +12,7 @@ open Util open Names open Term open Vars -open Closure +open CClosure open Environ open Libnames open Globnames -- cgit v1.2.3