From 18ffccadd1901e666ea3600263454446f52849d8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 9 Dec 2002 08:40:00 +0000
Subject: Ajout Simpl et Change sur des sous-termes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3392 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/tacexpr.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 521a08bc2b..dc163ea210 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -152,7 +152,8 @@ type ('constr,'cst,'ind,'id) gen_atomic_tactic_expr =
 
   (* Conversion *)
   | TacReduce of ('constr,'cst) red_expr_gen * 'id raw_hyp_location list
-  | TacChange of 'constr * 'id raw_hyp_location list
+  | TacChange of
+      'constr occurrences option * 'constr * 'id raw_hyp_location list
 
   (* Equivalence relations *)
   | TacReflexivity
-- 
cgit v1.2.3