diff options
Diffstat (limited to 'plugins/quote')
| -rw-r--r-- | plugins/quote/quote.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 23069a9ab..fc9d70ae7 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -225,8 +225,9 @@ let compute_rhs env sigma bodyi index_of_f = let compute_ivs f cs gl = let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - let cst = try destConst sigma f with DestKO -> i_can't_do_that () in - let body = Environ.constant_value_in (Global.env()) cst in + let (cst, u) = try destConst sigma f with DestKO -> i_can't_do_that () in + let u = EInstance.kind sigma u in + let body = Environ.constant_value_in (Global.env()) (cst, u) in let body = EConstr.of_constr body in match decomp_term sigma body with | Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) -> |