diff options
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/extract_env.ml | 2 | ||||
| -rw-r--r-- | plugins/extraction/extraction.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index f7d78551d8..a0627dbe63 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -581,7 +581,7 @@ let rec locate_ref = function with Nametab.GlobalizationError _ | UserError _ -> None in match mpo, ro with - | None, None -> Nametab.error_global_not_found qid + | None, None -> Nametab.error_global_not_found ~info:Exninfo.null qid | None, Some r -> let refs,mps = locate_ref l in r::refs,mps | Some mp, None -> let refs,mps = locate_ref l in refs,mp::mps | Some mp, Some r -> 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) |