diff options
| author | Enrico Tassi | 2018-05-31 16:08:59 +0200 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-04-02 21:20:26 +0200 |
| commit | 3a10b4d89d3d0ba3cdc8f85fbe3b66e8653da117 (patch) | |
| tree | 2362a4fe02299bae7dd18d5f1c354920270bce24 /plugins | |
| parent | bf4fdaa1836a17e4d36d38ba47959d1f50155a7b (diff) | |
[ssr] move is_ind/constructor_ref to ssrcommon
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 4 | ||||
| -rw-r--r-- | plugins/ssr/ssrcommon.mli | 3 | ||||
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 7 |
3 files changed, 8 insertions, 6 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 2a84469af0..ec9a937f80 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1540,5 +1540,9 @@ let get g = end +let is_construct_ref sigma c r = + EConstr.isConstruct sigma c && GlobRef.equal (ConstructRef (fst(EConstr.destConstruct sigma c))) r +let is_ind_ref sigma c r = EConstr.isInd sigma c && GlobRef.equal (IndRef (fst(EConstr.destInd sigma c))) r + (* vim: set filetype=ocaml foldmethod=marker: *) diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 9662daa7c7..585db41de0 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -482,3 +482,6 @@ module MakeState(S : StateType) : sig val get : Proofview.Goal.t -> S.state end + +val is_ind_ref : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool +val is_construct_ref : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index ccd0203b17..f55ece7d09 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -19,7 +19,6 @@ open Context open Vars open Locus open Printer -open Globnames open Termops open Tacinterp @@ -381,10 +380,6 @@ let pirrel_rewrite ?(under=false) pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl (Pp.fnl()++str"Rule's type:" ++ spc() ++ pr_econstr_env env sigma hd_ty)) ;; -let is_construct_ref sigma c r = - EConstr.isConstruct sigma c && GlobRef.equal (ConstructRef (fst(EConstr.destConstruct sigma c))) r -let is_ind_ref sigma c r = EConstr.isInd sigma c && GlobRef.equal (IndRef (fst(EConstr.destInd sigma c))) r - let rwcltac ?under cl rdx dir sr gl = let sr = let sigma, r = sr in @@ -403,7 +398,7 @@ let rwcltac ?under cl rdx dir sr gl = let sigma, c_ty = Typing.type_of env sigma c in ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty)); match EConstr.kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with - | AtomicType(e, a) when is_ind_ref sigma e c_eq -> + | AtomicType(e, a) when Ssrcommon.is_ind_ref sigma e c_eq -> let new_rdx = if dir = L2R then a.(2) else a.(1) in pirrel_rewrite ?under cl rdx rdxt new_rdx dir (sigma,c) c_ty, tclIDTAC, gl | _ -> |