From 7862ba932d53b1b0874564ef40e6f2d37ec690a1 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Fri, 28 May 2010 12:27:28 +0000
Subject: Correction program_simplify. Devrait corriger certaines contribs.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13031 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Program/Tactics.v | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'theories/Program')

diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index f4d53c2791..a000cdc24d 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -302,10 +302,8 @@ Ltac refine_hyp c :=
    possibly using [program_simplify] to use standard goal-cleaning tactics. *)
 
 Ltac program_simplify :=
-(*  arnaud: enlever la première ligne en faveur de la suite. *)
-simpl ; intros ; destruct_conjs ; simpl proj1_sig in * ; subst* ; autoinjections ; try discriminates ;
-(*  arnaud: restore: simpl in |- *; intros ; destruct_all_rec_calls ; repeat (destruct_conjs; simpl proj1_sig in * );
-  subst*; autoinjections ; try discriminates ;*)
+simpl in |- *; intros ; destruct_all_rec_calls ; repeat (destruct_conjs; simpl proj1_sig in * );
+  subst*; autoinjections ; try discriminates ;
     try (solve [ red ; intros ; destruct_conjs ; autoinjections ; discriminates ]).
 
 Ltac program_solve_wf :=
-- 
cgit v1.2.3