diff options
Diffstat (limited to 'plugins/setoid_ring')
| -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 0f996c65a..d0fe1f957 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) (CAst.make @@ GVar(Id.of_string"t"),None)); + [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (DAst.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" |