diff options
| author | herbelin | 2001-10-11 17:27:20 +0000 |
|---|---|---|
| committer | herbelin | 2001-10-11 17:27:20 +0000 |
| commit | 301a70e45eac43f034077c95bce04edbcf2ab4ad (patch) | |
| tree | d61c92f0d7a46203618a4610301c64d65c9c03ad /pretyping/pattern.ml | |
| parent | 1d5b3f16e202af2874181671abd86a47fca37cd7 (diff) | |
Suppression option immediate_discharge; nettoyage de Declare et conséquences
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2109 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |