From 870bc5c4badfa48556e473ad7b14c9d36b42d53d Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 8 Apr 2009 20:23:46 +0000
Subject: Experimental support for automatic destruction of recursive calls and
 clearing of recursive protototypes in Program obligations. Relies on marking
 said prototypes with a particular constant and preprocessing obligation goals
 with an appropriate tactic.

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

(limited to 'theories/Program')

diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index fff78a85af..25385a77a5 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -185,6 +185,18 @@ Tactic Notation "destruct_call" constr(f) "in" hyp(id) :=
 Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) "in" hyp(id) := 
   destruct_call_as_in f l id.
 
+(** A marker for prototypes to destruct. *)
+
+Definition fix_proto {A : Type} (a : A) := a.
+
+Ltac destruct_rec_calls :=
+  match goal with
+    | [ H : fix_proto _ |- _ ] => destruct_calls H ; clear H
+  end.
+
+Ltac destruct_all_rec_calls := 
+  repeat destruct_rec_calls ; unfold fix_proto in *.
+
 (** Try to inject any potential constructor equality hypothesis. *)
 
 Ltac autoinjection tac :=
@@ -252,7 +264,8 @@ Ltac refine_hyp c :=
    possibly using [program_simplify] to use standard goal-cleaning tactics. *)
 
 Ltac program_simplify :=
-  simpl ; intros ; 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_simpl := program_simplify ; auto.
-- 
cgit v1.2.3