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