diff options
Diffstat (limited to 'tactics/eauto.ml')
| -rw-r--r-- | tactics/eauto.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 2408b8f2b..3df9e3f82 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -89,7 +89,7 @@ let rec prolog l n gl = let out_term env = function | IsConstr (c, _) -> c - | IsGlobRef gr -> EConstr.of_constr (fst (Universes.fresh_global_instance env gr)) + | IsGlobRef gr -> EConstr.of_constr (fst (UnivGen.fresh_global_instance env gr)) let prolog_tac l n = Proofview.V82.tactic begin fun gl -> |