From 60e0c5e7018fd6532456c2c1909d537813469c85 Mon Sep 17 00:00:00 2001
From: delahaye
Date: Tue, 24 Apr 2001 19:47:43 +0000
Subject: Suppression d'une partie de code commente

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1700 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/field/Field_Tactic.v | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/contrib/field/Field_Tactic.v b/contrib/field/Field_Tactic.v
index f19a3d5bc2..4b676e8bbd 100644
--- a/contrib/field/Field_Tactic.v
+++ b/contrib/field/Field_Tactic.v
@@ -223,9 +223,6 @@ Tactic Definition InverseTest FT :=
 (**** Field itself ****)
 
 Tactic Definition ApplySimplif sfun :=
-(*  Match Context With
-  | [ |- (interp_ExprA ?1 ?2 ?3)==(interp_ExprA ? ?4 ?5) ] ->
-    (sfun ?1 ?2 ?3);(sfun ?1 ?4 ?5).*)
   (Match Context With
    | [ |- (interp_ExprA ?1 ?2 ?3)==(interp_ExprA ? ? ?) ] ->
      (sfun ?1 ?2 ?3));
-- 
cgit v1.2.3