aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/pfedit.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/pfedit.ml')
-rw-r--r--proofs/pfedit.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 777870249..b1cf3764e 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -219,7 +219,8 @@ let solve_nth k tac =
let by tac = mutate (solve_pftreestate tac)
-let instantiate_nth_evar_com n c = mutate (instantiate_pf_com n c)
+let instantiate_nth_evar_com n c =
+ mutate (instantiate_pf_com n c)
let traverse n = mutate (traverse n)