diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index c7a0dfe7a9..a9fc90df26 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -17,7 +17,6 @@ open Univ open Evd open Declarations open Environ -open Instantiate open Closure open Esubst open Reduction @@ -428,7 +427,7 @@ let whd_betadeltaiota_nolet env sigma x = let rec whd_evar sigma c = match kind_of_term c with | Evar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev -> - whd_evar sigma (Instantiate.existential_value sigma (ev,args)) + whd_evar sigma (Evd.existential_value sigma (ev,args)) | _ -> collapse_appl c let nf_evar sigma = |