diff options
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 |