diff options
| author | Maxime Dénès | 2020-05-14 16:33:15 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-05-14 16:33:15 +0200 |
| commit | 81fba800a97955368791df115e807cde66eff19c (patch) | |
| tree | c0cb601061912a95a8b5ad031f0378a1e479320b /plugins/extraction | |
| parent | 8dd5c47007817c104d57a449409a6b9c6f8ef12e (diff) | |
| parent | 101d898869ffa07fc772b303e3dbb7ecd860386b (diff) | |
Merge PR #11922: No more local reduction functions in Reductionops.
Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: gares
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/extraction.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index afc83b780b..0f96b9bbe8 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -259,7 +259,7 @@ let parse_ind_args si args relmax = let rec extract_type env sg db j c args = - match EConstr.kind sg (whd_betaiotazeta sg c) with + match EConstr.kind sg (whd_betaiotazeta env sg c) with | App (d, args') -> (* We just accumulate the arguments. *) extract_type env sg db j d (Array.to_list args' @ args) @@ -380,7 +380,7 @@ and extract_type_app env sg db (r,s) args = and extract_type_scheme env sg db c p = if Int.equal p 0 then extract_type env sg db 0 c [] else - let c = whd_betaiotazeta sg c in + let c = whd_betaiotazeta env sg c in match EConstr.kind sg c with | Lambda (n,t,d) -> extract_type_scheme (push_rel_assum (n,t) env) sg db d (p-1) |