diff options
| author | Pierre-Marie Pédrot | 2014-06-12 15:04:06 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-06-12 15:20:36 +0200 |
| commit | bda7852cb0896727389935f420eec0e8e3315cf7 (patch) | |
| tree | dc03858224a7dfbd3b92c0aee016356ab9dda6ce /plugins/decl_mode | |
| parent | a4db087565dd2ecfa3bcc022277bed1a3c868fd3 (diff) | |
Passing some tactics to the new monad type.
Diffstat (limited to 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 97989e2687..c230a98963 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -437,7 +437,7 @@ let thus_tac c ctyp submetas gls = with Not_found -> error "I could not relate this statement to the thesis." in if List.is_empty list then - exact_check proof gls + Proofview.V82.of_tactic (exact_check proof) gls else let refiner = concl_refiner list proof gls in Tactics.refine refiner gls @@ -534,14 +534,14 @@ let instr_rew _thus rew_side cut gls0 = tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id new_eq)) [tclTHEN tcl_erase_info (tclTHENS (Proofview.V82.of_tactic (transitivity lhs)) - [just_tac;exact_check (mkVar last_id)]); + [just_tac;Proofview.V82.of_tactic (exact_check (mkVar last_id))]); thus_tac new_eq] gls0 | Rhs -> let new_eq = mkApp(Lazy.force _eq,[|typ;lhs;cut.cut_stat.st_it|]) in tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id new_eq)) [tclTHEN tcl_erase_info (tclTHENS (Proofview.V82.of_tactic (transitivity rhs)) - [exact_check (mkVar last_id);just_tac]); + [Proofview.V82.of_tactic (exact_check (mkVar last_id));just_tac]); thus_tac new_eq] gls0 |