From dc5169d0e4bdf6569c3776aff819bfcb383379a9 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 16 Sep 2002 08:42:17 +0000
Subject: Subst (tout court)

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

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 801c9c85f7..da35ef0d1c 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1237,3 +1237,13 @@ let rec subst = function
   | [] -> tclIDTAC
   | x :: r -> tclTHEN (subst_one x) (subst r)
 
+let subst_all gl =
+  let eqpat = build_coq_eq_pattern () in
+  let test (_,c) =
+    if not (is_matching eqpat c) then failwith "caught";
+    let (_,x,_) = match_eq eqpat c in
+    match kind_of_term x with Var x -> x | _ -> failwith "caught"
+  in
+  let ids = map_succeed test (pf_hyps_types gl) in
+  let ids = list_uniquize ids in
+  subst ids gl
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 57715afdcc..871444c216 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -92,3 +92,5 @@ val discriminable : env -> evar_map -> constr -> constr -> bool
 (* Subst *)
 
 val subst : identifier list -> tactic
+val subst_all : tactic
+
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index b1aa23179a..6907acd355 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -219,5 +219,6 @@ END
 
 TACTIC EXTEND Subst
 | [ "Subst" ne_ident_list(l) ] -> [ subst l ]
+| [ "Subst" ] -> [ subst_all ]
 END
 
-- 
cgit v1.2.3