diff options
| author | Emilio Jesus Gallego Arias | 2019-06-21 22:50:08 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-08 15:59:10 +0200 |
| commit | c51fb2fae0e196012de47203b8a71c61720d6c5c (patch) | |
| tree | e49c2d38b6c841dc6514944750d21ed08ab94bce /pretyping/constr_matching.ml | |
| parent | 437063a0c745094c5693d1c5abba46ce375d69c6 (diff) | |
[api] Deprecate GlobRef constructors.
Not pretty, but it had to be done some day, as `Globnames` seems to be
on the way out.
I have taken the opportunity to reduce the number of `open` in the
codebase.
The qualified style would indeed allow us to use a bit nicer names
`GlobRef.Inductive` instead of `IndRef`, etc... once we have the
tooling to do large-scale refactoring that could be tried.
Diffstat (limited to 'pretyping/constr_matching.ml')
| -rw-r--r-- | pretyping/constr_matching.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 415b9ec6df..e85c888b2e 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -15,7 +15,6 @@ open Util open Names open Constr open Context -open Globnames open Termops open EConstr open Vars @@ -237,11 +236,12 @@ let merge_binding sigma allow_bound_rels ctx n cT subst = else raise PatternMatchingFailure in constrain sigma n c subst - + let matches_core env sigma allow_bound_rels (binding_vars,pat) c = let open EConstr in - let convref ref c = + let convref ref c = + let open GlobRef in match ref, EConstr.kind sigma c with | VarRef id, Var id' -> Names.Id.equal id id' | ConstRef c, Const (c',_) -> Constant.equal c c' @@ -270,7 +270,7 @@ let matches_core env sigma allow_bound_rels | PMeta None, m -> subst - | PRef (VarRef v1), Var v2 when Id.equal v1 v2 -> subst + | PRef (GlobRef.VarRef v1), Var v2 when Id.equal v1 v2 -> subst | PVar v1, Var v2 when Id.equal v1 v2 -> subst @@ -307,7 +307,7 @@ let matches_core env sigma allow_bound_rels | PApp (c1,arg1), App (c2,arg2) -> (match c1, EConstr.kind sigma c2 with - | PRef (ConstRef r), Proj (pr,c) when not (Constant.equal r (Projection.constant pr)) + | PRef (GlobRef.ConstRef r), Proj (pr,c) when not (Constant.equal r (Projection.constant pr)) || Projection.unfolded pr -> raise PatternMatchingFailure | PProj (pr1,c1), Proj (pr,c) -> @@ -323,7 +323,7 @@ let matches_core env sigma allow_bound_rels try Array.fold_left2 (sorec ctx env) (sorec ctx env subst c1 c2) arg1 arg2 with Invalid_argument _ -> raise PatternMatchingFailure) - | PApp (PRef (ConstRef c1), _), Proj (pr, c2) + | PApp (PRef (GlobRef.ConstRef c1), _), Proj (pr, c2) when Projection.unfolded pr || not (Constant.equal c1 (Projection.constant pr)) -> raise PatternMatchingFailure |