From f4d930d2e7ca21348ac51050c4821fd9c31760ab Mon Sep 17 00:00:00 2001 From: msozeau Date: Wed, 14 Mar 2007 16:46:25 +0000 Subject: Add destruct_call_concl in SubtacTactics and fix obvious obligation handling bug introduced by previous commit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9704 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/subtac/SubtacTactics.v | 13 +++++++++++++ contrib/subtac/subtac_obligations.ml | 5 ++--- 2 files changed, 15 insertions(+), 3 deletions(-) (limited to 'contrib/subtac') diff --git a/contrib/subtac/SubtacTactics.v b/contrib/subtac/SubtacTactics.v index 1d4d948ac..0a935c0d2 100644 --- a/contrib/subtac/SubtacTactics.v +++ b/contrib/subtac/SubtacTactics.v @@ -49,6 +49,19 @@ Ltac destruct_call f := end end. +Ltac destruct_call_concl f := + match goal with + | |- ?T => + match T with + | context [f ?x ?y ?z ?w ?v ?u] => let n := fresh "H" in set (n:=f x y z w v u); destruct n + | context [f ?x ?y ?z ?w ?v] => let n := fresh "H" in set (n:=f x y z w v); destruct n + | context [f ?x ?y ?z ?w] => let n := fresh "H" in set (n:=f x y z w); destruct n + | context [f ?x ?y ?z] => let n := fresh "H" in set (n:=f x y z); destruct n + | context [f ?x ?y] => let n := fresh "H" in set (n:=f x y); destruct n + | context [f ?x] => let n := fresh "H" in set (n:=f x); destruct n + end + end. + Ltac myinjection := let tac H := inversion H ; subst ; clear H in match goal with diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index d42de1333..b15dd97b1 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -240,9 +240,8 @@ let update_obls prg obls rem = (declare_mutual_definition progs; from_prg := List.fold_left (fun acc x -> - ProgMap.remove x.prg_name acc) !from_prg progs; - true) - else false) + ProgMap.remove x.prg_name acc) !from_prg progs); + false) let is_defined obls x = obls.(x).obl_body <> None -- cgit v1.2.3