diff options
| author | Pierre-Marie Pédrot | 2016-04-18 14:39:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-04 13:47:12 +0200 |
| commit | de4b9b68445d9f3e48da789404cbdfcd89214585 (patch) | |
| tree | aa383a63227fd77df70b8cc5c374ca7f08334ccf /ltac/tacinterp.ml | |
| parent | d2f0db714bd2d393423cf2dcb4ed37913029e052 (diff) | |
Moving the Val module to Geninterp.
Diffstat (limited to 'ltac/tacinterp.ml')
| -rw-r--r-- | ltac/tacinterp.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 6e76b19106..f39a42271b 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -30,6 +30,7 @@ open Term open Termops open Tacexpr open Genarg +open Geninterp open Stdarg open Constrarg open Printer @@ -118,7 +119,9 @@ type tacvalue = | VRec of value Id.Map.t ref * glob_tactic_expr let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) = - Genarg.create_arg "tacvalue" + let wit = Genarg.create_arg "tacvalue" in + let () = register_val0 wit None in + wit let of_tacvalue v = in_gen (topwit wit_tacvalue) v let to_tacvalue v = out_gen (topwit wit_tacvalue) v |