diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-01 02:36:16 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-01 20:19:53 +0200 |
| commit | 7babf0d42af11f5830bc157a671bd81b478a4f02 (patch) | |
| tree | 428ee1f95355ee5e11c19e12d538e37cc5a81f6c /plugins/quote | |
| parent | 3df2431a80f9817ce051334cb9c3b1f465bffb60 (diff) | |
Using delayed universe instances in EConstr.
The transition has been done a bit brutally. I think we can still save a
lot of useless normalizations here and there by providing the right API
in EConstr. Nonetheless, this is a first step.
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 |])) -> |