diff options
Diffstat (limited to 'pretyping/pattern.ml')
| -rw-r--r-- | pretyping/pattern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 54e67e401c..253e3e579d 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -161,7 +161,7 @@ let matches_core convert pat c = | PVar v1, IsVar v2 when v1 = v2 -> sigma - | PRef ref, _ when Declare.constr_of_reference Evd.empty (Global.env()) ref = cT -> sigma + | PRef ref, _ when Declare.constr_of_reference ref = cT -> sigma | PRel n1, IsRel n2 when n1 = n2 -> sigma @@ -184,7 +184,7 @@ let matches_core convert pat c = | PRef (ConstRef _ as ref), _ when convert <> None -> let (env,evars) = out_some convert in - let c = Declare.constr_of_reference Evd.empty env ref in + let c = Declare.constr_of_reference ref in if is_conv env evars c cT then sigma else raise PatternMatchingFailure |