aboutsummaryrefslogtreecommitdiff
path: root/plugins/firstorder/rules.ml
diff options
context:
space:
mode:
authorMaxime Dénès2018-05-06 17:19:58 +0200
committerMaxime Dénès2018-05-06 17:19:58 +0200
commitdad4731deed5c09e4e6cb212cd81462f7896c363 (patch)
tree413c52bbb7c67c228e20434ef2dfd6bd59c86753 /plugins/firstorder/rules.ml
parent87c959542e1bed55b14d371f1be02cd60d89082c (diff)
parentafceace455a4b37ced7e29175ca3424996195f7b (diff)
Merge PR #6156: [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.
Diffstat (limited to 'plugins/firstorder/rules.ml')
-rw-r--r--plugins/firstorder/rules.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index cfcd656191..2d7a3e37b7 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -29,7 +29,7 @@ type tactic = unit Proofview.tactic
type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
-type lseqtac= global_reference -> seqtac
+type lseqtac= GlobRef.t -> seqtac
type 'a with_backtracking = tactic -> 'a