diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-08 18:14:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-08 18:14:53 +0200 |
| commit | 9fe0471ef0127e9301d0450aacaeb1690abb82ad (patch) | |
| tree | 6a244976f5caef6a2b88c84053fce87f94c78f96 /pretyping | |
| 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 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 2 | ||||
| -rw-r--r-- | pretyping/pretyping.mli | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 5e6a3eac7..21eb100b4 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -49,7 +49,7 @@ open Context.Named.Declaration type typing_constraint = OfType of types | IsType | WithoutTypeConstraint type var_map = constr_under_binders Id.Map.t type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t -type unbound_ltac_var_map = Genarg.Val.t Id.Map.t +type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t type ltac_var_map = { ltac_constrs : var_map; ltac_uconstrs : uconstr_var_map; diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 91320f20a..824bb11aa 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -29,7 +29,7 @@ type typing_constraint = OfType of types | IsType | WithoutTypeConstraint type var_map = Pattern.constr_under_binders Id.Map.t type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t -type unbound_ltac_var_map = Genarg.Val.t Id.Map.t +type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t type ltac_var_map = { ltac_constrs : var_map; |