diff options
| author | Gaëtan Gilbert | 2018-06-23 15:08:55 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-07-24 12:03:10 +0200 |
| commit | 7817af48a554573fb649028263ecfc0fabe400d8 (patch) | |
| tree | 1298a503c997f8246fe726142f4fa8b2121c97e8 | |
| parent | fb9003c7850c459d7a5981212d8ef87de877bd9f (diff) | |
Remove useless is_projection in tacred
| -rw-r--r-- | pretyping/tacred.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 40c4cfaa45..869d14c627 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -49,7 +49,7 @@ let error_not_evaluable r = let is_evaluable_const env cst = is_transparent env (ConstKey cst) && - (evaluable_constant cst env || is_projection cst env) + evaluable_constant cst env let is_evaluable_var env id = is_transparent env (VarKey id) && evaluable_named id env |