From 9c352481f1a2d3a9c2e0e1f084d1c65521a0c438 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 19 Sep 2016 20:00:19 +0200
Subject: Merging Stdarg and Constrarg.

There was no reason to keep them separate since quite a long time. Historically,
they were making Genarg depend or not on upper strata of the code, but since
it was moved to lib/ this is not justified anymore.
---
 plugins/setoid_ring/g_newring.ml4 | 1 -
 plugins/setoid_ring/newring.ml    | 4 ++--
 2 files changed, 2 insertions(+), 3 deletions(-)

(limited to 'plugins/setoid_ring')

diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index 13e2254044..0987c44ae2 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -15,7 +15,6 @@ open Printer
 open Newring_ast
 open Newring
 open Stdarg
-open Constrarg
 open Tacarg
 open Pcoq.Constr
 open Pltac
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index a5e2211d81..657efe175b 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -124,8 +124,8 @@ let closed_term_ast l =
   let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in
   TacFun([Some(Id.of_string"t")],
   TacML(Loc.ghost,tacname,
-  [TacGeneric (Genarg.in_gen (Genarg.glbwit Constrarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None));
-   TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Constrarg.wit_ref)) l)]))
+  [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (GVar(Loc.ghost,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"
 *)
-- 
cgit v1.2.3