diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2core.ml | 1 | ||||
| -rw-r--r-- | src/tac2quote.ml | 2 | ||||
| -rw-r--r-- | src/tac2quote.mli | 2 |
3 files changed, 5 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 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 |