diff options
Diffstat (limited to 'plugins/firstorder/instances.mli')
| -rw-r--r-- | plugins/firstorder/instances.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli index 61786ffdc..9f9ade3aa 100644 --- a/plugins/firstorder/instances.mli +++ b/plugins/firstorder/instances.mli @@ -8,13 +8,13 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Globnames +open Names open Rules val collect_quantified : Evd.evar_map -> Sequent.t -> Formula.t list * Sequent.t val give_instances : Evd.evar_map -> Formula.t list -> Sequent.t -> - (Unify.instance * global_reference) list + (Unify.instance * GlobRef.t) list val quantified_tac : Formula.t list -> seqtac with_backtracking |