diff options
| author | Pierre-Marie Pédrot | 2016-05-08 18:14:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-08 18:14:53 +0200 |
| commit | 9fe0471ef0127e9301d0450aacaeb1690abb82ad (patch) | |
| tree | 6a244976f5caef6a2b88c84053fce87f94c78f96 /dev | |
| parent | a6de02fcfde76f49b10d8481a2423692fa105756 (diff) | |
| parent | 8d3f0b614d7b2fb30f6e87b48a4fc5c0d286e49c (diff) | |
Change the toplevel representation of Ltac values to an untyped one.
This brings the evaluation model of Ltac closer to those of usual languages, and
further allows the integration of static typing in the long run. More precisely,
toplevel constructed values such as lists and the like do not carry anymore the
type of the underlying data they contain.
This is mostly an API change, as it did not break any contrib outside of mathcomp.
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 *) |