diff options
| author |  bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-09-06 14:29:09 +0000 |
|---|---|---|
| committer | bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-09-06 14:29:09 +0000 |
| commit | 620f17a49046892d7e355fd953ecf06e82088b40 (patch) | |
| tree | 7f5ae6675d99f8f85e244c9d18715a88446d9517 /contrib | |
| parent | c71049de672ab2dec8e13fd2810b4c76e215a947 (diff) | |
errors in recdef.ml4:
a few errors of parentheses around fun x -> ... constructs,
a use of tclTHEN was left over from bug tracking modifications, it
was badly parenthesized.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10117 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/recdef/recdef.ml4 | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index 06f6c1856..832e4647f 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -293,10 +293,10 @@ let mkCaseEq a : tactic = let type_of_a = pf_type_of g a in tclTHENLIST [h_generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]; - fun g2 -> + (fun g2 -> change_in_concl None (pattern_occs [([-1], a)] (pf_env g2) Evd.empty (pf_concl g2)) - g2; + g2); simplest_case a] g);; (* This is like the previous one except that it also rewrite on all @@ -320,9 +320,9 @@ let mkDestructEq : to_revert_constr in tclTHENLIST [h_generalize new_hyps; - fun g2 -> + (fun g2 -> change_in_concl None - (pattern_occs [([-1], expr)] (pf_env g2) Evd.empty (pf_concl g2)) g2; + (pattern_occs [([-1], expr)] (pf_env g2) Evd.empty (pf_concl g2)) g2); simplest_case expr], to_revert let rec mk_intros_and_continue thin_intros (extra_eqn:bool) @@ -1246,7 +1246,7 @@ let rec prove_eq (termine:constr) (f:constr)(functional:global_reference) (fun g -> let destruct_tac,rev_to_thin_intro = mkDestructEq [] a g in tclTHENS - (tclTHEN destruct_tac + destruct_tac (list_map_i (fun i -> mk_intros_and_continue (List.rev rev_to_thin_intro) true |