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/ssr/ssrequality.ml | |
| parent | bf4fdaa1836a17e4d36d38ba47959d1f50155a7b (diff) | |
[ssr] move is_ind/constructor_ref to ssrcommon
Diffstat (limited to 'plugins/ssr/ssrequality.ml')
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 7 |
1 files changed, 1 insertions, 6 deletions
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 | _ -> |