diff options
author | Stephane Glondu <steph@glondu.net> | 2014-07-27 10:02:38 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2014-07-27 10:02:38 +0200 |
commit | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (patch) | |
tree | 8b5450c5801a1592e0348ad0362f950e7bb958d4 /plugins/funind/functional_principles_proofs.ml | |
parent | d2c5c5e616a6e118291fe1ce9965c731adac03a8 (diff) |
Imported Upstream version 8.4pl4dfsgupstream/8.4pl4dfsg
Diffstat (limited to 'plugins/funind/functional_principles_proofs.ml')
-rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 48205019..b5876ffa 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -188,7 +188,7 @@ let prove_trivial_eq h_id context (constructor,type_of_term,term) = let find_rectype env c = - let (t, l) = decompose_app (Reduction.whd_betadeltaiota env c) in + let (t, l) = decompose_app (Reduction.whd_betaiotazeta c) in match kind_of_term t with | Ind ind -> (t, l) | Construct _ -> (t,l) @@ -576,7 +576,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = onLastHypId (fun heq_id -> tclTHENLIST [ (* Then the new hypothesis *) tclMAP introduction_no_check dyn_infos.rec_hyps; - (* observe_tac "after_introduction" *)(fun g' -> + observe_tac "after_introduction" (fun g' -> (* We get infos on the equations introduced*) let new_term_value_eq = pf_type_of g' (mkVar heq_id) in (* compute the new value of the body *) @@ -603,7 +603,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = } in clean_goal_with_heq ptes_infos continue_tac new_infos g' - )]) + )]) ] g |