Removing SortArgType.

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

3 files changed, 10 insertions, 20 deletions

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