diff options
| author | Pierre-Marie Pédrot | 2016-04-20 15:09:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-04 13:47:12 +0200 |
| commit | 1c999a9760f4f2287d11529600ec96567e630ce6 (patch) | |
| tree | bd3651d5db44d0546dca6e81bf8773aa58770936 | |
| parent | a2a8840a4fe1b3d6c6dbc27b5521b28bd319ff42 (diff) | |
Do not generate generic arguments for data which only requires toplevel values.
| -rw-r--r-- | ltac/tauto.ml | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/ltac/tauto.ml b/ltac/tauto.ml index c075d05bbf..7cda8d9147 100644 --- a/ltac/tauto.ml +++ b/ltac/tauto.ml @@ -55,14 +55,13 @@ type tauto_flags = { strict_unit : bool; } -let wit_tauto_flags : tauto_flags uniform_genarg_type = - let wit = Genarg.create_arg "tauto_flags" in - let () = register_val0 wit None in - wit +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 @@ -259,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.inject (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)]))) |