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 /ltac/tauto.ml | |
| 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 'ltac/tauto.ml')
| -rw-r--r-- | ltac/tauto.ml | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/ltac/tauto.ml b/ltac/tauto.ml index a86fdb98a..7cda8d914 100644 --- a/ltac/tauto.ml +++ b/ltac/tauto.ml @@ -11,6 +11,7 @@ open Hipattern open Names open Pp open Genarg +open Geninterp open Stdarg open Misctypes open Tacexpr @@ -54,12 +55,13 @@ type tauto_flags = { strict_unit : bool; } -let wit_tauto_flags : tauto_flags uniform_genarg_type = - Genarg.create_arg "tauto_flags" +let tag_tauto_flags : tauto_flags Val.typ = Val.create "tauto_flags" -let assoc_flags ist = - let v = Id.Map.find (Names.Id.of_string "tauto_flags") ist.lfun in - try Value.cast (topwit wit_tauto_flags) v with _ -> assert false +let assoc_flags ist : tauto_flags = + let Val.Dyn (tag, v) = Id.Map.find (Names.Id.of_string "tauto_flags") ist.lfun in + match Val.eq tag tag_tauto_flags with + | None -> assert false + | Some Refl -> v (* Whether inner not are unfolded *) let negation_unfolding = ref true @@ -256,7 +258,7 @@ let tauto_power_flags = { let with_flags flags _ ist = let f = (loc, Id.of_string "f") in let x = (loc, Id.of_string "x") in - let arg = Val.Dyn (val_tag (topwit wit_tauto_flags), flags) in + let arg = Val.Dyn (tag_tauto_flags, flags) in let ist = { ist with lfun = Id.Map.add (snd x) arg ist.lfun } in eval_tactic_ist ist (TacArg (loc, TacCall (loc, ArgVar f, [Reference (ArgVar x)]))) |