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/cc/g_congruence.ml4 | 1 - plugins/derive/g_derive.ml4 | 2 +- plugins/extraction/g_extraction.ml4 | 1 - plugins/firstorder/g_ground.ml4 | 3 +-- plugins/funind/g_indfun.ml4 | 2 +- plugins/micromega/g_micromega.ml4 | 2 +- plugins/omega/g_omega.ml4 | 2 +- plugins/quote/g_quote.ml4 | 2 +- plugins/romega/g_romega.ml4 | 2 +- plugins/setoid_ring/g_newring.ml4 | 1 - plugins/setoid_ring/newring.ml | 4 ++-- plugins/ssrmatching/ssrmatching.ml4 | 2 +- 12 files changed, 10 insertions(+), 14 deletions(-) (limited to 'plugins') diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4 index 52a135119..6f6811334 100644 --- a/plugins/cc/g_congruence.ml4 +++ b/plugins/cc/g_congruence.ml4 @@ -10,7 +10,6 @@ open Cctac open Stdarg -open Constrarg DECLARE PLUGIN "cc_plugin" diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4 index d4dc7e0ee..deadb3b4d 100644 --- a/plugins/derive/g_derive.ml4 +++ b/plugins/derive/g_derive.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Constrarg +open Stdarg (*i camlp4deps: "grammar/grammar.cma" i*) diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 19fda4aea..e1d6bb4a8 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -14,7 +14,6 @@ DECLARE PLUGIN "extraction_plugin" open Genarg open Stdarg -open Constrarg open Pcoq.Prim open Pp open Names diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 487162687..344a04a6a 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -15,9 +15,8 @@ open Goptions open Tacticals open Tacinterp open Libnames -open Constrarg -open Tacarg open Stdarg +open Tacarg open Pcoq.Prim DECLARE PLUGIN "ground_plugin" diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 6368c2536..6603a95a8 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -14,7 +14,7 @@ open Constrexpr open Indfun_common open Indfun open Genarg -open Constrarg +open Stdarg open Misctypes open Pcoq.Prim open Pcoq.Constr diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index aadcf060e..79020ed03 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -16,7 +16,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Constrarg +open Stdarg open Tacarg DECLARE PLUGIN "micromega_plugin" diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index 5647fbf9f..27115abec 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -19,7 +19,7 @@ DECLARE PLUGIN "omega_plugin" open Names open Coq_omega -open Constrarg +open Stdarg let eval_tactic name = let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index ebd19428f..e7e6ecef9 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -13,7 +13,7 @@ open Misctypes open Tacexpr open Geninterp open Quote -open Constrarg +open Stdarg open Tacarg DECLARE PLUGIN "quote_plugin" diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index 830dc54dd..2f38688d1 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -12,7 +12,7 @@ DECLARE PLUGIN "romega_plugin" open Names open Refl_omega -open Constrarg +open Stdarg let eval_tactic name = let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index 13e225404..0987c44ae 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 a5e2211d8..657efe175 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" *) diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 099918c35..bedf925e8 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -19,7 +19,7 @@ open Names open Pp open Pcoq open Genarg -open Constrarg +open Stdarg open Tacarg open Term open Vars -- cgit v1.2.3