diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-01-23 10:01:33 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-01-23 10:01:33 +0100 |
| commit | 2e798fb83db743ce44350af6f7f9442811f374ad (patch) | |
| tree | c21f8be141617491622fdb1f9adf62cfc3026ed9 /pretyping | |
| parent | 89d14fa4f16e9741108887177d43d34675261d22 (diff) | |
| parent | fe0e62bebcd71aca8b56cc615d81667a31e43388 (diff) | |
Merge PR #6627: Fix #6619: coqchk does not reduce compatibility constants for primitive projections
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/tacred.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 5a522e06a..f682143f8 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -60,9 +60,7 @@ let value_of_evaluable_ref env evref u = match evref with | EvalConstRef con -> let u = Unsafe.to_instance u in - EConstr.of_constr (try constant_value_in env (con,u) - with NotEvaluableConst IsProj -> - raise (Invalid_argument "value_of_evaluable_ref")) + EConstr.of_constr (constant_value_in env (con, u)) | EvalVarRef id -> env |> lookup_named id |> NamedDecl.get_value |> Option.get let evaluable_of_global_reference env = function |