aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/setoid_ring/newring.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-04-09 03:35:20 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-04-25 00:33:36 +0200
commitee2197096fe75a63b4d92cb3a1bb05122c5c625b (patch)
tree3b40c06375a463625a2675b90e009fcb0b64a7d2 /plugins/setoid_ring/newring.ml
parent054d2736c1c1b55cb7708ff0444af521cd0fe2ba (diff)
[location] [ast] Port module AST to CAst
Diffstat (limited to 'plugins/setoid_ring/newring.ml')
-rw-r--r--plugins/setoid_ring/newring.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index e2a6ad55c..2b64204c9 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -131,7 +131,7 @@ let closed_term_ast l =
let l = List.map (fun gr -> ArgArg(Loc.tag gr)) l in
TacFun([Name(Id.of_string"t")],
TacML(Loc.tag (tacname,
- [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (Loc.tag @@ GVar(Id.of_string"t"),None));
+ [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (CAst.make @@ GVar(Id.of_string"t"),None));
TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)])))
(*
let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"