diff options
| author | Pierre-Marie Pédrot | 2015-01-21 00:26:59 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-01-21 00:46:06 +0100 |
| commit | c2d053c6f38a54e3083c8726eccb3e73942107b7 (patch) | |
| tree | 2eef9978ece47590799ab97acfe9043e213b8d40 /plugins | |
| parent | 9cc95f5a34b9050fe5a869f0fb96da562b45353d (diff) | |
Embedding the index of the ML tactic entry in the Tacexpr AST.
This will allow to get rid of the fragile mechanism of discriminating which
entry to call depending on the dynamic type of its arguments.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/setoid_ring/newring.ml4 | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 2f9e8509c2..72ebfae486 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -143,6 +143,10 @@ let closed_term_ast l = mltac_plugin = "newring_plugin"; mltac_tactic = "closed_term"; } in + let tacname = { + mltac_name = tacname; + mltac_index = 0; + } in let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in TacFun([Some(Id.of_string"t")], TacML(Loc.ghost,tacname, |