diff options
Diffstat (limited to 'ltac/tacinterp.ml')
| -rw-r--r-- | ltac/tacinterp.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 167501de2..20ad9fd4b 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -691,7 +691,9 @@ let interp_pure_open_constr ist = let interp_typed_pattern ist env sigma (_,c,_) = let sigma, c = interp_gen WithoutTypeConstraint ist true pure_open_constr_flags env sigma c in - pattern_of_constr env sigma c + (** FIXME: it is necessary to be unsafe here because of the way we handle + evars in the pretyper. Sometimes they get solved eagerly. *) + pattern_of_constr env sigma (EConstr.Unsafe.to_constr c) (* Interprets a constr expression *) let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l = @@ -736,7 +738,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = try Inl (coerce_to_evaluable_ref env sigma x) with CannotCoerceTo _ -> let c = coerce_to_closed_constr env x in - Inr (pattern_of_constr env sigma c) in + Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (loc,id) with Not_found -> error_global_not_found ~loc (qualid_of_ident id)) |