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 /dev | |
| parent | d2f0db714bd2d393423cf2dcb4ed37913029e052 (diff) | |
Moving the Val module to Geninterp.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/printers.mllib | 2 | ||||
| -rw-r--r-- | dev/top_printers.ml | 4 |
2 files changed, 4 insertions, 2 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index 9f25ba55e7..5d10f54fb2 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -146,6 +146,8 @@ Typeclasses_errors Logic_monad Proofview_monad Proofview +Ftactic +Geninterp Typeclasses Detyping Indrec diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 29ea08e025..f9c1971a82 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -467,8 +467,8 @@ let pp_generic_argument arg = pp(str"<genarg:"++pr_argument_type(genarg_tag arg)++str">") let prgenarginfo arg = - let Val.Dyn (tag, _) = arg in - let tpe = Val.pr tag in + let Geninterp.Val.Dyn (tag, _) = arg in + let tpe = Geninterp.Val.pr tag in (** FIXME *) (* try *) (* let data = Pptactic.pr_top_generic (Global.env ()) arg in *) |