diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-18 00:02:45 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-18 01:15:43 +0200 |
| commit | 243ffa4b928486122075762da6ce8da707e07daf (patch) | |
| tree | 3870e1b1d3059ba13158a73df7c5f3b300e504ce /plugins | |
| parent | 6dd9e003c289a79b0656e7c6f2cc59935997370c (diff) | |
Moving the TacExtend node from atomic to plain tactics.
Also taking advantage of the change to rename it into TacML. Ultimately
should allow ML tactic to return values.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/setoid_ring/newring.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 8ba3319de..2647ca22a 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -145,9 +145,9 @@ let closed_term_ast l = } in let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in TacFun([Some(Id.of_string"t")], - TacAtom(Loc.ghost,TacExtend(Loc.ghost,tacname, + TacML(Loc.ghost,tacname, [Genarg.in_gen (Genarg.glbwit Constrarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None); - Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Constrarg.wit_ref)) l]))) + Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Constrarg.wit_ref)) l])) (* let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term" *) |