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.

5 files changed, 105 insertions, 142 deletions

diff --git a/interp/constrarg.ml b/interp/constrarg.ml
deleted file mode 100644
index b8baa6401..000000000
--- a/interp/constrarg.ml
+++ /dev/null
@@ -1,66 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Loc
-open Misctypes
-open Tactypes
-open Genarg
-open Geninterp
-
-let make0 ?dyn name =
-  let wit = Genarg.make0 name in
-  let () = Geninterp.register_val0 wit dyn in
-  wit
-
-(** This is a hack for now, to break the dependency of Genarg on constr-related
-    types. We should use dedicated functions someday. *)
-
-let loc_of_or_by_notation f = function
-  | AN c -> f c
-  | ByNotation (loc,s,_) -> loc
-
-let wit_int_or_var =
-  make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) "int_or_var"
-
-let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type =
-  make0 "intropattern"
-
-let wit_ident =
-  make0 "ident"
-
-let wit_var =
-  make0 ~dyn:(val_tag (topwit wit_ident)) "var"
-
-let wit_ref = make0 "ref"
-
-let wit_quant_hyp = make0 "quant_hyp"
-
-let wit_constr =
-  make0 "constr"
-
-let wit_uconstr = make0 "uconstr"
-
-let wit_open_constr = make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr"
-
-let wit_constr_with_bindings = make0 "constr_with_bindings"
-
-let wit_bindings = make0 "bindings"
-
-let wit_red_expr = make0 "redexpr"
-
-let wit_clause_dft_concl  =
-  make0 "clause_dft_concl"
-
-(** Aliases *)
-
-let wit_reference = wit_ref
-let wit_global = wit_ref
-let wit_clause = wit_clause_dft_concl
-let wit_quantified_hypothesis = wit_quant_hyp
-let wit_intropattern = wit_intro_pattern
-let wit_redexpr = wit_red_expr
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
deleted file mode 100644
index 4b542675b..000000000
--- a/interp/constrarg.mli
+++ /dev/null
@@ -1,75 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** Generic arguments based on [constr]. We put them here to avoid a dependency
-    of Genarg in [constr]-related interfaces. *)
-
-open Loc
-open Names
-open Term
-open Libnames
-open Globnames
-open Genredexpr
-open Pattern
-open Constrexpr
-open Misctypes
-open Tactypes
-open Genarg
-
-(** FIXME: nothing to do there. *)
-val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t
-
-(** {5 Additional generic arguments} *)
-
-val wit_int_or_var : (int or_var, int or_var, int) genarg_type
-
-val wit_intro_pattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type
-
-val wit_ident : Id.t uniform_genarg_type
-
-val wit_var : (Id.t located, Id.t located, Id.t) genarg_type
-
-val wit_ref : (reference, global_reference located or_var, global_reference) genarg_type
-
-val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
-
-val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type
-
-val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type
-
-val wit_open_constr :
-  (constr_expr, glob_constr_and_expr, constr) genarg_type
-
-val wit_constr_with_bindings :
-  (constr_expr with_bindings,
-  glob_constr_and_expr with_bindings,
-  constr with_bindings delayed_open) genarg_type
-
-val wit_bindings :
-  (constr_expr bindings,
-  glob_constr_and_expr bindings,
-  constr bindings delayed_open) genarg_type
-
-val wit_red_expr :
-  ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
-  (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
-  (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
-
-val wit_clause_dft_concl :  (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
-
-(** Aliases for compatibility *)
-
-val wit_reference : (reference, global_reference located or_var, global_reference) genarg_type
-val wit_global : (reference, global_reference located or_var, global_reference) genarg_type
-val wit_clause :  (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
-val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type
-val wit_intropattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type
-val wit_redexpr :
-  ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
-  (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
-  (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
diff --git a/interp/interp.mllib b/interp/interp.mllib
index 96b52959a..607af82a0 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -1,5 +1,4 @@
 Stdarg
-Constrarg
 Genintern
 Constrexpr_ops
 Notation_ops
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 2a7d52e3a..341ff5662 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -6,6 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Loc
+open Misctypes
+open Tactypes
 open Genarg
 open Geninterp
 
@@ -29,7 +32,49 @@ let wit_string : string uniform_genarg_type =
 let wit_pre_ident : string uniform_genarg_type =
   make0 ~dyn:(val_tag (topwit wit_string)) "preident"
 
+let loc_of_or_by_notation f = function
+  | AN c -> f c
+  | ByNotation (loc,s,_) -> loc
+
+let wit_int_or_var =
+  make0 ~dyn:(val_tag (topwit wit_int)) "int_or_var"
+
+let wit_intro_pattern =
+  make0 "intropattern"
+
+let wit_ident =
+  make0 "ident"
+
+let wit_var =
+  make0 ~dyn:(val_tag (topwit wit_ident)) "var"
+
+let wit_ref = make0 "ref"
+
+let wit_quant_hyp = make0 "quant_hyp"
+
+let wit_constr =
+  make0 "constr"
+
+let wit_uconstr = make0 "uconstr"
+
+let wit_open_constr = make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr"
+
+let wit_constr_with_bindings = make0 "constr_with_bindings"
+
+let wit_bindings = make0 "bindings"
+
+let wit_red_expr = make0 "redexpr"
+
+let wit_clause_dft_concl  =
+  make0 "clause_dft_concl"
+
 (** Aliases for compatibility *)
 
 let wit_integer = wit_int
 let wit_preident = wit_pre_ident
+let wit_reference = wit_ref
+let wit_global = wit_ref
+let wit_clause = wit_clause_dft_concl
+let wit_quantified_hypothesis = wit_quant_hyp
+let wit_intropattern = wit_intro_pattern
+let wit_redexpr = wit_red_expr
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index e1f648d7f..af3a73462 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -8,8 +8,21 @@
 
 (** Basic generic arguments. *)
 
+open Loc
+open Names
+open Term
+open Libnames
+open Globnames
+open Genredexpr
+open Pattern
+open Constrexpr
+open Misctypes
+open Tactypes
 open Genarg
 
+(** FIXME: nothing to do there. *)
+val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t
+
 val wit_unit : unit uniform_genarg_type
 
 val wit_bool : bool uniform_genarg_type
@@ -20,7 +33,54 @@ val wit_string : string uniform_genarg_type
 
 val wit_pre_ident : string uniform_genarg_type
 
+(** {5 Additional generic arguments} *)
+
+val wit_int_or_var : (int or_var, int or_var, int) genarg_type
+
+val wit_intro_pattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type
+
+val wit_ident : Id.t uniform_genarg_type
+
+val wit_var : (Id.t located, Id.t located, Id.t) genarg_type
+
+val wit_ref : (reference, global_reference located or_var, global_reference) genarg_type
+
+val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
+
+val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type
+
+val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type
+
+val wit_open_constr :
+  (constr_expr, glob_constr_and_expr, constr) genarg_type
+
+val wit_constr_with_bindings :
+  (constr_expr with_bindings,
+  glob_constr_and_expr with_bindings,
+  constr with_bindings delayed_open) genarg_type
+
+val wit_bindings :
+  (constr_expr bindings,
+  glob_constr_and_expr bindings,
+  constr bindings delayed_open) genarg_type
+
+val wit_red_expr :
+  ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
+  (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
+  (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
+
+val wit_clause_dft_concl :  (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
+
 (** Aliases for compatibility *)
 
 val wit_integer : int uniform_genarg_type
 val wit_preident : string uniform_genarg_type
+val wit_reference : (reference, global_reference located or_var, global_reference) genarg_type
+val wit_global : (reference, global_reference located or_var, global_reference) genarg_type
+val wit_clause :  (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
+val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type
+val wit_intropattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type
+val wit_redexpr :
+  ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
+  (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
+  (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type