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/cases.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/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 20dec96ef4..a562204b54 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -367,7 +367,7 @@ let make_return_predicate_ltac_lvar env sigma na tm c = - if [c] is a variable [id'], then [x] should now become [id'] - otherwise, [x] should be hidden *) match na, DAst.get tm with - | Name id, (GVar id' | GRef (Globnames.VarRef id', _)) when Id.equal id id' -> + | Name id, (GVar id' | GRef (GlobRef.VarRef id', _)) when Id.equal id id' -> let expansion = match kind sigma c with | Var id' -> Name id' | _ -> Anonymous in |