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 /plugins/firstorder/formula.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 'plugins/firstorder/formula.ml')
| -rw-r--r-- | plugins/firstorder/formula.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 2d5ea9536c..fb363b9393 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -15,7 +15,6 @@ open EConstr open Vars open Util open Declarations -open Globnames module RelDecl = Context.Rel.Declaration @@ -124,7 +123,7 @@ type side = Hyp | Concl | Hint let no_atoms = (false,{positive=[];negative=[]}) -let dummy_id=VarRef (Id.of_string "_") (* "_" cannot be parsed *) +let dummy_id=GlobRef.VarRef (Id.of_string "_") (* "_" cannot be parsed *) let build_atoms env sigma metagen side cciterm = let trivial =ref false |