From c881773b7893e819e6d85c79f3a9293d970bbe3f Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 11 Sep 2002 15:06:35 +0000
Subject: tactique Subst x1 ... xn

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2998 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/equality.ml      | 6 +++++-
 tactics/equality.mli     | 2 +-
 tactics/extratactics.ml4 | 2 +-
 3 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 73626f07b8..801c9c85f7 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1206,7 +1206,7 @@ let is_eq_x x c =
   (let (_,y,_) = match_eq eqpat c in
    match kind_of_term y with Var y -> x = y | _ -> false)
 
-let subst x gl = 
+let subst_one x gl = 
   let varx = mkVar x in
   let hyps = pf_hyps_types gl in
   let hyp = 
@@ -1233,3 +1233,7 @@ let subst x gl =
     tclTRY (clear [x])
   ] gl
 
+let rec subst = function
+  | [] -> tclIDTAC
+  | x :: r -> tclTHEN (subst_one x) (subst r)
+
diff --git a/tactics/equality.mli b/tactics/equality.mli
index e92e251bdf..57715afdcc 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -91,4 +91,4 @@ val discriminable : env -> evar_map -> constr -> constr -> bool
 
 (* Subst *)
 
-val subst : identifier -> tactic
+val subst : identifier list -> tactic
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index c211892133..b1aa23179a 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -218,6 +218,6 @@ END
 (* Subst *)
 
 TACTIC EXTEND Subst
-| [ "Subst" ident(x) ] -> [ subst x ]
+| [ "Subst" ne_ident_list(l) ] -> [ subst l ]
 END
 
-- 
cgit v1.2.3