Moving (e)transitivity out of the AST.

9 files changed, 9 insertions, 15 deletions

diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 6a413ca31..e152cdd7f 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -409,7 +409,6 @@ let rec mlexpr_of_atomic_tactic = function
 
   (* Equivalence relations *)
   | Tacexpr.TacSymmetry ido -> <:expr< Tacexpr.TacSymmetry $mlexpr_of_clause ido$ >>
-  | Tacexpr.TacTransitivity c -> <:expr< Tacexpr.TacTransitivity $mlexpr_of_option mlexpr_of_constr c$ >>
 
   (* Automation tactics *)
   | Tacexpr.TacAuto (debug,n,lems,l) ->
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 5a7a20ef6..223ece63b 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -157,7 +157,6 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
 
   (* Equivalence relations *)
   | TacSymmetry of 'nam clause_expr
-  | TacTransitivity of 'trm option
 
   (* Equality and inversion *)
   | TacRewrite of evars_flag *
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 4ac7a5bff..3e80c99f5 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -652,8 +652,6 @@ GEXTEND Gram
 
       (* Equivalence relations *)
       | IDENT "symmetry"; cl = clause_dft_concl -> TacSymmetry cl
-      | IDENT "transitivity"; c = constr -> TacTransitivity (Some c)
-      | IDENT "etransitivity" -> TacTransitivity None
 
       (* Equality and inversion *)
       | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ",";
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 0ea8b4048..a5b07c477 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -790,8 +790,6 @@ and pr_atom1 = function
 
   (* Equivalence relations *)
   | TacSymmetry cls -> str "symmetry" ++ pr_clauses (Some true) pr_ident cls
-  | TacTransitivity (Some c) -> str "transitivity" ++ pr_constrarg c
-  | TacTransitivity None -> str "etransitivity"
 
   (* Equality and inversion *)
   | TacRewrite (ev,l,cl,by) ->
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index d3b9dd132..f033ef5ca 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -23,6 +23,10 @@ TACTIC EXTEND assumption
   [ "assumption" ] -> [ Tactics.assumption ]
 END
 
+TACTIC EXTEND etransitivity
+  [ "etransitivity" ] -> [ Tactics.intros_transitivity None ]
+END
+
 TACTIC EXTEND cut
   [ "cut" constr(c) ] -> [ Tactics.cut c ]
 END
@@ -46,3 +50,7 @@ END
 TACTIC EXTEND lapply
   [ "lapply" constr(c) ] -> [ Tactics.cut_and_apply c ]
 END
+
+TACTIC EXTEND transitivity
+  [ "transitivity" constr(c) ] -> [ Tactics.intros_transitivity (Some c) ]
+END
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 22ea274cb..3b1cdecfb 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -554,7 +554,6 @@ let rec intern_atomic lf ist x =
   (* Equivalence relations *)
   | TacSymmetry idopt ->
       TacSymmetry (clause_app (intern_hyp_location ist) idopt)
-  | TacTransitivity c -> TacTransitivity (Option.map (intern_constr ist) c)
 
   (* Equality and inversion *)
   | TacRewrite (ev,l,cl,by) ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a992c52ce..12547e704 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1772,12 +1772,6 @@ and interp_atomic ist tac =
         let cl = interp_clause ist env c in
         Tactics.intros_symmetry cl
       end
-  | TacTransitivity c ->
-      begin match c with
-      | None -> Tactics.intros_transitivity None
-      | Some c ->
-          (new_interp_constr ist c) (fun c -> Tactics.intros_transitivity (Some c))
-      end
 
   (* Equality and inversion *)
   | TacRewrite (ev,l,cl,by) ->
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 4d0b59569..1b15fa8e1 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -195,7 +195,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
 
   (* Equivalence relations *)
   | TacSymmetry _ as x -> x
-  | TacTransitivity c -> TacTransitivity (Option.map (subst_glob_constr subst) c)
 
   (* Equality and inversion *)
   | TacRewrite (ev,l,cl,by) ->
diff --git a/theories/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v
index 6b6c85310..f49c51e1e 100644
--- a/theories/Numbers/NatInt/NZSqrt.v
+++ b/theories/Numbers/NatInt/NZSqrt.v
@@ -66,7 +66,7 @@ Qed.
 Lemma sqrt_unique : forall a b, b² <= a < (S b)² -> √a == b.
 Proof.
  intros a b (LEb,LTb).
- assert (Ha : 0<=a) by (transitivity b²; trivial using square_nonneg).
+ assert (Ha : 0<=a) by (transitivity (b²); trivial using square_nonneg).
  assert (Hb : 0<=b) by (apply sqrt_spec_nonneg; order).
  assert (Ha': 0<=√a) by now apply sqrt_nonneg.
  destruct (sqrt_spec a Ha) as (LEa,LTa).