diff options
Diffstat (limited to 'plugins/funind/indfun_common.mli')
| -rw-r--r-- | plugins/funind/indfun_common.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index bb59a5c9c..8f80c072c 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -117,9 +117,9 @@ val h_intros: Names.identifier list -> Proof_type.tactic val h_id : Names.identifier val hrec_id : Names.identifier val acc_inv_id : Term.constr Util.delayed -val ltof_ref : Libnames.global_reference Util.delayed +val ltof_ref : Globnames.global_reference Util.delayed val well_founded_ltof : Term.constr Util.delayed val acc_rel : Term.constr Util.delayed val well_founded : Term.constr Util.delayed -val evaluable_of_global_reference : Libnames.global_reference -> Names.evaluable_global_reference +val evaluable_of_global_reference : Globnames.global_reference -> Names.evaluable_global_reference val list_rewrite : bool -> (Term.constr*bool) list -> Proof_type.tactic |