From c2e3d63ca60b27abb5398ecbc8ebcaf8fb925206 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 18 Jan 2008 19:41:43 +0000
Subject: Fix bug #1778, better typeclass error messages. Move Obligations
 Tactic to a wrapper around Ltac program_simpl ::= . !!!! This may introduce
 incompatibilities because now modifications of program_simpl are properly
 handled and work across modules.

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

(limited to 'theories/Program')

diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index c3870e6bda..ad03de2f40 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -175,4 +175,6 @@ Ltac program_simplify :=
   simpl ; intros ; destruct_conjs ; simpl proj1_sig in * ; subst* ; try autoinjection ; try discriminates ;
     try (solve [ red ; intros ; destruct_conjs ; try autoinjection ; discriminates ]).
 
-Ltac program_simpl := program_simplify ; auto with *.
+Ltac default_program_simpl := program_simplify ; auto with *.
+
+Ltac program_simpl := default_program_simpl.
-- 
cgit v1.2.3