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 /parsing | |
| 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 'parsing')
| -rw-r--r-- | parsing/pcoq.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index e60b470fdf..53d2089c04 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -730,9 +730,7 @@ let () = Grammar.register0 wit_var (Prim.var); Grammar.register0 wit_ref (Prim.reference); Grammar.register0 wit_quant_hyp (Tactic.quantified_hypothesis); - Grammar.register0 wit_sort (Constr.sort); Grammar.register0 wit_constr (Constr.constr); - Grammar.register0 wit_constr_may_eval (Tactic.constr_may_eval); Grammar.register0 wit_uconstr (Tactic.uconstr); Grammar.register0 wit_open_constr (Tactic.open_constr); Grammar.register0 wit_constr_with_bindings (Tactic.constr_with_bindings); |