diff options
Diffstat (limited to 'plugins/ssr')
| -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. *) |