From 087012f8d3e5e31f489e35dce8397b5202c928b6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 2 Aug 2017 01:57:48 +0200
Subject: Adding the open_constr scope

---
 src/tac2core.ml   | 1 +
 src/tac2quote.ml  | 2 ++
 src/tac2quote.mli | 2 ++
 3 files changed, 5 insertions(+)

(limited to 'src')

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
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index 488bcb5201..0e0a7b3fce 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -55,6 +55,8 @@ let of_ident ?loc id = inj_wit ?loc Stdarg.wit_ident id
 
 let of_constr ?loc c = inj_wit ?loc Stdarg.wit_constr c
 
+let of_open_constr ?loc c = inj_wit ?loc Stdarg.wit_open_constr c
+
 let of_bool ?loc b =
   let c = if b then Core.c_true else Core.c_false in
   constructor ?loc c []
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index c9ee270d38..a311430a66 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -30,6 +30,8 @@ val of_ident : ?loc:Loc.t -> Id.t -> raw_tacexpr
 
 val of_constr : ?loc:Loc.t -> Constrexpr.constr_expr -> raw_tacexpr
 
+val of_open_constr : ?loc:Loc.t -> Constrexpr.constr_expr -> raw_tacexpr
+
 val of_list : ?loc:Loc.t -> raw_tacexpr list -> raw_tacexpr
 
 val of_bindings : ?loc:Loc.t -> bindings -> raw_tacexpr
-- 
cgit v1.2.3