diff options
| author | Gaëtan Gilbert | 2020-02-07 15:18:39 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-07 15:18:39 +0100 |
| commit | 51c0b1414be9a46e221b13f652474db0194093fc (patch) | |
| tree | 8b260deab34b79ee2a251f65e9de75c2b292dd36 /plugins | |
| parent | e2d25ea2b9df57ba4006cbc9c04b8f0dfbd2733a (diff) | |
Remove confusing commented code in funind
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 19 |
1 files changed, 8 insertions, 11 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 6db0a1119b..00f4be783d 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1573,19 +1573,16 @@ let prove_principle_for_gen (List.rev_map (get_name %> Nameops.Name.get_id) (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params) ); - (* observe_tac "" *) Proofview.V82.of_tactic (assert_by - (Name acc_rec_arg_id) - (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|])) - (Proofview.V82.tactic prove_rec_arg_acc) - ); -(* observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids))); -(* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++ *) -(* str "fix arg num" ++ int (List.length args_ids + 1) ); tclIDTAC g); *) - (* observe_tac "h_fix " *) (Proofview.V82.of_tactic (fix fix_id (List.length args_ids + 1))); -(* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_unsafe_type_of g (mkVar fix_id) )); tclIDTAC g); *) + Proofview.V82.of_tactic + (assert_by + (Name acc_rec_arg_id) + (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|])) + (Proofview.V82.tactic prove_rec_arg_acc)); + (revert (List.rev (acc_rec_arg_id::args_ids))); + (Proofview.V82.of_tactic (fix fix_id (List.length args_ids + 1))); h_intros (List.rev (acc_rec_arg_id::args_ids)); Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref)); - (* observe_tac "finish" *) (fun gl' -> + (fun gl' -> let body = let _,args = destApp (project gl') (pf_concl gl') in Array.last args |