Removing useless generic arguments.

8 files changed, 6 insertions, 27 deletions

diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 99f0a2da64..b8f97e77c3 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -46,9 +46,6 @@ let wit_ref = make0 "ref"
 
 let wit_quant_hyp = make0 "quant_hyp"
 
-let wit_sort : (glob_sort, glob_sort, sorts) genarg_type =
-  make0 "sort"
-
 let wit_constr =
   make0 "constr"
 
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index 6407b61afd..70c9c0de2c 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -38,15 +38,8 @@ val wit_ref : (reference, global_reference located or_var, global_reference) gen
 
 val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
 
-val wit_sort : (glob_sort, glob_sort, sorts) genarg_type
-
 val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type
 
-val wit_constr_may_eval :
-  ((constr_expr,reference or_by_notation,constr_expr) may_eval,
-  (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) may_eval,
-  constr) genarg_type
-
 val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type
 
 val wit_open_constr :
@@ -62,8 +55,6 @@ val wit_bindings :
   glob_constr_and_expr bindings,
   constr bindings delayed_open) genarg_type
 
-val wit_hyp_location_flag : Locus.hyp_location_flag uniform_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,
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 925c1679f2..79f80260fa 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -393,6 +393,12 @@ open Leminv
 
 let seff id = Vernacexpr.VtSideff [id], Vernacexpr.VtLater
 
+VERNAC ARGUMENT EXTEND sort
+| [ "Set" ] -> [ GSet ]
+| [ "Prop" ] -> [ GProp ]
+| [ "Type" ] -> [ GType [] ]
+END
+
 VERNAC COMMAND EXTEND DeriveInversionClear
 | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort(s) ]
   => [ seff na ]
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index 15589d5c4a..977c56f38b 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -800,7 +800,6 @@ let () =
   Genintern.register_intern0 wit_var (lift intern_hyp);
   Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg);
   Genintern.register_intern0 wit_ltac (lift intern_tactic_or_tacarg);
-  Genintern.register_intern0 wit_sort (fun ist s -> (ist, s));
   Genintern.register_intern0 wit_quant_hyp (lift intern_quantified_hypothesis);
   Genintern.register_intern0 wit_constr (fun ist c -> (ist,intern_constr ist c));
   Genintern.register_intern0 wit_uconstr (fun ist c -> (ist,intern_constr ist c));
@@ -808,7 +807,6 @@ let () =
   Genintern.register_intern0 wit_red_expr (lift intern_red_expr);
   Genintern.register_intern0 wit_bindings (lift intern_bindings);
   Genintern.register_intern0 wit_constr_with_bindings (lift intern_constr_with_bindings);
-  Genintern.register_intern0 wit_constr_may_eval (lift intern_constr_may_eval);
   ()
 
 (***************************************************************************)
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 94c13a0e0e..a9baef79c7 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -2104,14 +2104,12 @@ let () =
   register_interp0 wit_intro_pattern (lifts interp_intro_pattern);
   register_interp0 wit_clause_dft_concl (lift interp_clause);
   register_interp0 wit_constr (lifts interp_constr);
-  register_interp0 wit_sort (lifts (fun _ _ evd s -> interp_sort evd s));
   register_interp0 wit_tacvalue (fun ist v -> Ftactic.return v);
   register_interp0 wit_red_expr (lifts interp_red_expr);
   register_interp0 wit_quant_hyp (lift interp_declared_or_quantified_hypothesis);
   register_interp0 wit_open_constr (lifts interp_open_constr);
   register_interp0 wit_bindings interp_bindings';
   register_interp0 wit_constr_with_bindings interp_constr_with_bindings';
-  register_interp0 wit_constr_may_eval (lifts interp_constr_may_eval);
   ()
 
 let () =
diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml
index 438219f5a3..54d32f2666 100644
--- a/ltac/tacsubst.ml
+++ b/ltac/tacsubst.ml
@@ -301,7 +301,6 @@ let () =
   Genintern.register_subst0 wit_tactic subst_tactic;
   Genintern.register_subst0 wit_ltac subst_tactic;
   Genintern.register_subst0 wit_constr subst_glob_constr;
-  Genintern.register_subst0 wit_sort (fun _ v -> v);
   Genintern.register_subst0 wit_clause_dft_concl (fun _ v -> v);
   Genintern.register_subst0 wit_uconstr (fun subst c -> subst_glob_constr subst c);
   Genintern.register_subst0 wit_open_constr (fun subst c -> subst_glob_constr subst c);
@@ -309,5 +308,4 @@ let () =
   Genintern.register_subst0 wit_quant_hyp subst_declared_or_quantified_hypothesis;
   Genintern.register_subst0 wit_bindings subst_bindings;
   Genintern.register_subst0 wit_constr_with_bindings subst_glob_with_bindings;
-  Genintern.register_subst0 wit_constr_may_eval subst_raw_may_eval;
   ()
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index e60b470fdf..53d2089c04 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -730,9 +730,7 @@ let () =
   Grammar.register0 wit_var (Prim.var);
   Grammar.register0 wit_ref (Prim.reference);
   Grammar.register0 wit_quant_hyp (Tactic.quantified_hypothesis);
-  Grammar.register0 wit_sort (Constr.sort);
   Grammar.register0 wit_constr (Constr.constr);
-  Grammar.register0 wit_constr_may_eval (Tactic.constr_may_eval);
   Grammar.register0 wit_uconstr (Tactic.uconstr);
   Grammar.register0 wit_open_constr (Tactic.open_constr);
   Grammar.register0 wit_constr_with_bindings (Tactic.constr_with_bindings);
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index a15fa772f8..6fb68ddf42 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1365,8 +1365,6 @@ let () =
     (pr_clauses (Some true) pr_lident)
     (pr_clauses (Some true) (fun id -> pr_lident (Loc.ghost,id)))
   ;
-  Genprint.register_print0 Constrarg.wit_sort
-    pr_glob_sort pr_glob_sort (pr_sort Evd.empty);
   Genprint.register_print0
     Constrarg.wit_constr
     Ppconstr.pr_constr_expr
@@ -1394,11 +1392,6 @@ let () =
     (pr_bindings_no_with pr_constr_expr pr_lconstr_expr)
     (pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
     (fun it -> pr_bindings_no_with pr_constr pr_lconstr (fst (run_delayed it)));
-  Genprint.register_print0 Constrarg.wit_constr_may_eval
-    (pr_may_eval pr_constr_expr pr_lconstr_expr (pr_or_by_notation pr_reference) pr_constr_pattern_expr)
-    (pr_may_eval (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)
-      (pr_or_var (pr_and_short_name pr_evaluable_reference)) (pr_pat_and_constr_expr pr_glob_constr))
-    pr_constr;
   Genprint.register_print0 Constrarg.wit_constr_with_bindings
     (pr_with_bindings pr_constr_expr pr_lconstr_expr)
     (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))