diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/subtac/SubtacTactics.v | 13 | ||||
| -rw-r--r-- | contrib/subtac/subtac_obligations.ml | 5 |
2 files changed, 15 insertions, 3 deletions
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 |