diff options
Diffstat (limited to 'plugins/subtac/subtac_pretyping.ml')
| -rw-r--r-- | plugins/subtac/subtac_pretyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml index a59cb96652..5b42c8ba5f 100644 --- a/plugins/subtac/subtac_pretyping.ml +++ b/plugins/subtac/subtac_pretyping.ml @@ -125,7 +125,7 @@ let subtac_process env isevars id bl c tycon = let imps = Option.default (Implicit_quantifiers.implicits_of_rawterm ~with_products:false c) imps in let coqc, ctyp = interp env isevars c tycon in let evm = non_instanciated_map env isevars !isevars in - let ty = nf_isevar !isevars (match tycon with Some (None, c) -> c | _ -> ctyp) in + let ty = nf_evar !isevars (match tycon with Some (None, c) -> c | _ -> ctyp) in evm, coqc, ty, imps open Subtac_obligations |