diff options
| author | Pierre-Marie Pédrot | 2020-10-29 13:59:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-12-21 13:55:32 +0100 |
| commit | 63332cbd4ac59b39fdce63d9872aa52dd8a2fec6 (patch) | |
| tree | 9913737179ee72e0c1b9672227fe5872ce6734a9 /plugins/ssr/ssrequality.ml | |
| parent | a714abe0a1c0cac277297f9e3c7f6d90ac0173d6 (diff) | |
Move evaluable_global_reference from Names to Tacred.
It is the only place where it starts making sense in the whole codebase. It also
fits nicely there since there are other functions manipulating this type in that
module.
In any case this type does not belong to the kernel.
Diffstat (limited to 'plugins/ssr/ssrequality.ml')
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index fdfba48024..723c786b4f 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -223,11 +223,11 @@ let simplintac occ rdx sim = end let rec get_evalref env sigma c = match EConstr.kind sigma c with - | Var id -> EvalVarRef id - | Const (k,_) -> EvalConstRef k + | Var id -> Tacred.EvalVarRef id + | Const (k,_) -> Tacred.EvalConstRef k | App (c', _) -> get_evalref env sigma c' | Cast (c', _, _) -> get_evalref env sigma c' - | Proj(c,_) -> EvalConstRef(Projection.constant c) + | Proj(c,_) -> Tacred.EvalConstRef(Projection.constant c) | _ -> errorstrm Pp.(str "The term " ++ pr_econstr_pat (Global.env ()) sigma c ++ str " is not unfoldable") (* Strip a pattern generated by a prenex implicit to its constant. *) |