diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-17 19:24:17 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-21 19:36:38 +0100 |
| commit | b2beb9087628de23679a831e6273b91816f1ed27 (patch) | |
| tree | 40784a3be039885aef29c3c23fda2a0189fe2ac1 /plugins | |
| parent | fcf425a4714f0c888b3d670a9a37fe52a6e49bc5 (diff) | |
Using dynamic values in tactic evaluation.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 2b07ba704..d596cf6fb 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -209,7 +209,7 @@ let get_res = let name = { mltac_plugin = "newring_plugin"; mltac_tactic = "get_res"; } in let entry = { mltac_name = name; mltac_index = 0 } in let tac args ist = - let n = Genarg.out_gen (Genarg.topwit Stdarg.wit_int) (List.hd args) in + let n = Tacinterp.Value.cast (Genarg.topwit Stdarg.wit_int) (List.hd args) in let init i = Id.Map.find (Id.of_string ("x" ^ string_of_int i)) ist.lfun in tactic_res := Array.init n init; Proofview.tclUNIT () |