From de4b9b68445d9f3e48da789404cbdfcd89214585 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 18 Apr 2016 14:39:34 +0200
Subject: Moving the Val module to Geninterp.

---
 tactics/taccoerce.ml  | 9 +++++++--
 tactics/taccoerce.mli | 1 +
 2 files changed, 8 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index 298257e45d..a03c529cc0 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -14,15 +14,20 @@ open Misctypes
 open Genarg
 open Stdarg
 open Constrarg
+open Geninterp
 
 exception CannotCoerceTo of string
 
 let (wit_constr_context : (Empty.t, Empty.t, constr) Genarg.genarg_type) =
-  Genarg.create_arg "constr_context"
+  let wit = Genarg.create_arg "constr_context" in
+  let () = register_val0 wit None in
+  wit
 
 (* includes idents known to be bound and references *)
 let (wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) Genarg.genarg_type) =
-  Genarg.create_arg "constr_under_binders"
+  let wit = Genarg.create_arg "constr_under_binders" in
+  let () = register_val0 wit None in
+  wit
 
 (** All the types considered here are base types *)
 let val_tag wit = match val_tag wit with
diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli
index 75a3b347d6..82e1910f7d 100644
--- a/tactics/taccoerce.mli
+++ b/tactics/taccoerce.mli
@@ -12,6 +12,7 @@ open Term
 open Misctypes
 open Pattern
 open Genarg
+open Geninterp
 
 (** Coercions from highest level generic arguments to actual data used by Ltac
     interpretation. Those functions examinate dynamic types and try to return
-- 
cgit v1.2.3