aboutsummaryrefslogtreecommitdiff
path: root/src/tac2core.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2017-08-25 18:02:49 +0200
committerPierre-Marie Pédrot2017-08-25 18:02:49 +0200
commit029dd0fcfc5641b689356c467e2f0fb1d3fa178c (patch)
treedafb824dfd334bf3af52f6188ae0d60338e4e65b /src/tac2core.ml
parent6875b016b0a502b03296e5f97f26cf0f6699a7aa (diff)
Renaming the bindings scope into with_bindings.
Diffstat (limited to 'src/tac2core.ml')
-rw-r--r--src/tac2core.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 7a8f3ceb44..342e8f51e8 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -912,7 +912,7 @@ let add_expr_scope name entry f =
end
let () = add_expr_scope "ident" q_ident (fun id -> Tac2quote.of_anti Tac2quote.of_ident id)
-let () = add_expr_scope "bindings" q_bindings Tac2quote.of_bindings
+let () = add_expr_scope "with_bindings" q_with_bindings Tac2quote.of_bindings
let () = add_expr_scope "intropattern" q_intropattern Tac2quote.of_intro_pattern
let () = add_expr_scope "intropatterns" q_intropatterns Tac2quote.of_intro_patterns
let () = add_expr_scope "induction_clause" q_induction_clause Tac2quote.of_induction_clause