Removing SortArgType.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16618 85f007b7-540e-0410-9357-904b9bb8a0f7

10 files changed, 19 insertions, 33 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 6d90af997d..e3efd196c6 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -358,7 +358,6 @@ let rec pr_argument_type = function
   | RefArgType -> str"ref"
   (* Specific types *)
   | GenArgType -> str"genarg"
-  | SortArgType -> str"sort"
   | ConstrArgType -> str"constr"
   | ConstrMayEvalArgType -> str"constr-may-eval"
   | QuantHypArgType -> str"qhyp"
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index d8f615a98f..128b13bdae 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -36,7 +36,6 @@ let rec make_wit loc = function
   | RefArgType -> <:expr< Constrarg.wit_ref >>
   | QuantHypArgType -> <:expr< Constrarg.wit_quant_hyp >>
   | GenArgType -> <:expr< Constrarg.wit_genarg >>
-  | SortArgType -> <:expr< Constrarg.wit_sort >>
   | ConstrArgType -> <:expr< Constrarg.wit_constr >>
   | ConstrMayEvalArgType -> <:expr< Constrarg.wit_constr_may_eval >>
   | RedExprArgType -> <:expr< Constrarg.wit_red_expr >>
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 9e8ff8b645..4b4f225455 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -211,7 +211,6 @@ let rec mlexpr_of_argtype loc = function
   | Genarg.BindingsArgType -> <:expr< Genarg.BindingsArgType >>
   | Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >>
   | Genarg.GenArgType -> <:expr< Genarg.GenArgType >>
-  | Genarg.SortArgType -> <:expr< Genarg.SortArgType >>
   | Genarg.ConstrArgType -> <:expr< Genarg.ConstrArgType >>
   | Genarg.ConstrMayEvalArgType -> <:expr< Genarg.ConstrMayEvalArgType >>
   | Genarg.ListArgType t -> <:expr< Genarg.ListArgType $mlexpr_of_argtype loc t$ >>
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 5c2b3392c4..16af7c3080 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -53,7 +53,8 @@ let wit_quant_hyp = unsafe_of_type QuantHypArgType
 
 let wit_genarg = unsafe_of_type GenArgType
 
-let wit_sort = unsafe_of_type SortArgType
+let wit_sort : (glob_sort, glob_sort, sorts) genarg_type =
+  Genarg.make0 None "sort"
 
 let wit_constr = unsafe_of_type ConstrArgType
 
@@ -75,4 +76,5 @@ let wit_red_expr = unsafe_of_type RedExprArgType
 
 let () =
   register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern";
-  register_name0 wit_tactic "Constrarg.wit_tactic"
+  register_name0 wit_tactic "Constrarg.wit_tactic";
+  register_name0 wit_sort "Constrarg.wit_sort";
diff --git a/lib/genarg.ml b/lib/genarg.ml
index 358a010aea..8e18be3d0c 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -17,7 +17,6 @@ type argument_type =
   | RefArgType
   (* Specific types *)
   | GenArgType
-  | SortArgType
   | ConstrArgType
   | ConstrMayEvalArgType
   | QuantHypArgType
@@ -36,7 +35,6 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
 | VarArgType, VarArgType -> true
 | RefArgType, RefArgType -> true
 | GenArgType, GenArgType -> true
-| SortArgType, SortArgType -> true
 | ConstrArgType, ConstrArgType -> true
 | ConstrMayEvalArgType, ConstrMayEvalArgType -> true
 | QuantHypArgType, QuantHypArgType -> true
diff --git a/lib/genarg.mli b/lib/genarg.mli
index a7232c6bd7..b8dd08f960 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -196,7 +196,6 @@ type argument_type =
   | RefArgType
   (** Specific types *)
   | GenArgType
-  | SortArgType
   | ConstrArgType
   | ConstrMayEvalArgType
   | QuantHypArgType
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 04a2ca1e30..8548a21b82 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -147,7 +147,6 @@ let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generi
   | VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x)
   | RefArgType -> prref (out_gen (rawwit wit_ref) x)
   | GenArgType -> pr_raw_generic prc prlc prtac prpat prref (out_gen (rawwit wit_genarg) x)
-  | SortArgType -> pr_glob_sort (out_gen (rawwit wit_sort) x)
   | ConstrArgType -> prc (out_gen (rawwit wit_constr) x)
   | ConstrMayEvalArgType ->
       pr_may_eval prc prlc (pr_or_by_notation prref) prpat
@@ -183,7 +182,6 @@ let rec pr_glb_generic prc prlc prtac prpat x =
   | VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x)
   | RefArgType -> pr_or_var (pr_located pr_global) (out_gen (glbwit wit_ref) x)
   | GenArgType -> pr_glb_generic prc prlc prtac prpat (out_gen (glbwit wit_genarg) x)
-  | SortArgType -> pr_glob_sort (out_gen (glbwit wit_sort) x)
   | ConstrArgType -> prc (out_gen (glbwit wit_constr) x)
   | ConstrMayEvalArgType ->
       pr_may_eval prc prlc
@@ -220,7 +218,6 @@ let rec pr_top_generic prc prlc prtac prpat x =
   | VarArgType -> pr_id (out_gen (topwit wit_var) x)
   | RefArgType -> pr_global (out_gen (topwit wit_ref) x)
   | GenArgType -> pr_top_generic prc prlc prtac prpat (out_gen (topwit wit_genarg) x)
-  | SortArgType -> pr_sort (out_gen (topwit wit_sort) x)
   | ConstrArgType -> prc (out_gen (topwit wit_constr) x)
   | ConstrMayEvalArgType -> prc (out_gen (topwit wit_constr_may_eval) x)
   | QuantHypArgType -> pr_quantified_hypothesis (out_gen (topwit wit_quant_hyp) x)
@@ -999,8 +996,11 @@ let pr_glob_tactic env = pr_glob_tactic_level env ltop
 let register_uniform_printer wit pr =
   Genprint.register_print0 wit pr pr pr
 
-let () = Genprint.register_print0 Constrarg.wit_intro_pattern
-  pr_intro_pattern pr_intro_pattern pr_intro_pattern
+let () =
+  Genprint.register_print0 Constrarg.wit_intro_pattern
+    pr_intro_pattern pr_intro_pattern pr_intro_pattern;
+  Genprint.register_print0 Constrarg.wit_sort
+    pr_glob_sort pr_glob_sort pr_sort
 
 let () =
   let printer _ _ prtac = prtac (0, E) in
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index d176c516ff..dbe8b8dd73 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -768,8 +768,6 @@ and intern_genarg ist x =
       in_gen (glbwit wit_ref) (intern_global_reference ist (out_gen (rawwit wit_ref) x))
   | GenArgType ->
       in_gen (glbwit wit_genarg) (intern_genarg ist (out_gen (rawwit wit_genarg) x))
-  | SortArgType ->
-      in_gen (glbwit wit_sort) (out_gen (rawwit wit_sort) x)
   | ConstrArgType ->
       in_gen (glbwit wit_constr) (intern_constr ist (out_gen (rawwit wit_constr) x))
   | ConstrMayEvalArgType ->
@@ -937,6 +935,8 @@ let add_tacdef local isrec tacl =
 
 (** Registering *)
 
+let lift intern = (); fun ist x -> (ist, intern ist x)
+
 let () =
   let intern_intro_pattern ist pat =
     let lf = ref Id.Set.empty in
@@ -947,8 +947,8 @@ let () =
   Genintern.register_intern0 wit_intro_pattern intern_intro_pattern
 
 let () =
-  let intern ist tac = (ist, intern_tactic_or_tacarg ist tac) in
-  Genintern.register_intern0 wit_tactic intern
+  Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg);
+  Genintern.register_intern0 wit_sort (fun ist s -> (ist, s))
 
 (***************************************************************************)
 (* Backwarding recursive needs of tactic glob/interp/eval functions *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index dea7cd5a2b..a7cfc08e98 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1397,14 +1397,6 @@ and interp_genarg ist gl x =
       in_gen (topwit wit_ref) (pf_interp_reference ist gl (out_gen (glbwit wit_ref) x))
     | GenArgType ->
       in_gen (topwit wit_genarg) (interp_genarg ist gl (out_gen (glbwit wit_genarg) x))
-    | SortArgType ->
-      let (sigma,c_interp) =
-	pf_interp_constr ist gl
-	  (GSort (dloc,out_gen (glbwit wit_sort) x), None)
-      in
-      evdref := sigma;
-      in_gen (topwit wit_sort)
-        (destSort c_interp)
     | ConstrArgType ->
       let (sigma,c_interp) = pf_interp_constr ist gl (out_gen (glbwit wit_constr) x) in
       evdref := sigma;
@@ -1879,8 +1871,6 @@ and interp_atomic ist gl tac =
         Value.of_constr (constr_of_global
           (pf_interp_reference ist gl (out_gen (glbwit wit_ref) x)))
     | GenArgType -> f (out_gen (glbwit wit_genarg) x)
-    | SortArgType ->
-        Value.of_constr (mkSort (interp_sort (out_gen (glbwit wit_sort) x)))
     | ConstrArgType ->
         let (sigma,v) = mk_constr_value ist gl (out_gen (glbwit wit_constr) x) in
 	evdref := sigma;
@@ -2017,7 +2007,9 @@ let () =
 
 let () =
   let interp ist gl pat = (gl.sigma, interp_intro_pattern ist gl pat) in
-  Geninterp.register_interp0 wit_intro_pattern interp
+  Geninterp.register_interp0 wit_intro_pattern interp;
+  let interp ist gl s = (gl.sigma, interp_sort s) in
+  Geninterp.register_interp0 wit_sort interp
 
 let () =
   let interp ist gl tac =
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 80a5633228..deac1d4ff1 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -296,8 +296,6 @@ and subst_genarg subst (x:glob_generic_argument) =
       in_gen (glbwit wit_ref) (subst_global_reference subst
 	(out_gen (glbwit wit_ref) x))
   | GenArgType -> in_gen (glbwit wit_genarg) (subst_genarg subst (out_gen (glbwit wit_genarg) x))
-  | SortArgType ->
-      in_gen (glbwit wit_sort) (out_gen (glbwit wit_sort) x)
   | ConstrArgType ->
       in_gen (glbwit wit_constr) (subst_glob_constr subst (out_gen (glbwit wit_constr) x))
   | ConstrMayEvalArgType ->
@@ -325,9 +323,9 @@ and subst_genarg subst (x:glob_generic_argument) =
 
 (** Registering *)
 
-let () = Genintern.register_subst0 wit_intro_pattern (fun _ v -> v)
-
 let () =
-  Genintern.register_subst0 wit_tactic subst_tactic
+  Genintern.register_subst0 wit_intro_pattern (fun _ v -> v);
+  Genintern.register_subst0 wit_tactic subst_tactic;
+  Genintern.register_subst0 wit_sort (fun _ v -> v)
 
 let _ = Hook.set Auto.extern_subst_tactic subst_tactic