aboutsummaryrefslogtreecommitdiff
path: root/src/tac2core.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2017-08-02 01:57:48 +0200
committerPierre-Marie Pédrot2017-08-02 02:00:42 +0200
commit087012f8d3e5e31f489e35dce8397b5202c928b6 (patch)
tree617863f4fddbdb75cbbd6a8c03ee3ca2d165e684 /src/tac2core.ml
parentd3c3859ab6dba6495b13e055917ddf3d95851912 (diff)
Adding the open_constr scope
Diffstat (limited to 'src/tac2core.ml')
-rw-r--r--src/tac2core.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 266e3b5f11..d2cc865299 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -876,3 +876,4 @@ let () = add_scope "intropatterns" begin function
end
let () = add_generic_scope "constr" Pcoq.Constr.constr Stdarg.wit_constr
+let () = add_generic_scope "open_constr" Pcoq.Constr.constr Stdarg.wit_open_constr