aboutsummaryrefslogtreecommitdiff
path: root/pretyping/patternops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/patternops.ml')
-rw-r--r--pretyping/patternops.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 2eff1936f4..b16d044956 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -220,6 +220,8 @@ let instantiate_pattern env sigma lvar c =
ctx
in
let c = substl inst c in
+ (** FIXME: Stupid workaround to pattern_of_constr being evar sensitive *)
+ let c = Evarutil.nf_evar sigma c in
pattern_of_constr env sigma (EConstr.Unsafe.to_constr c)
with Not_found (* List.index failed *) ->
let vars =