diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-06-12 15:04:06 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-06-12 15:20:36 +0200 |
| commit | bda7852cb0896727389935f420eec0e8e3315cf7 (patch) | |
| tree | dc03858224a7dfbd3b92c0aee016356ab9dda6ce /plugins/funind/invfun.ml | |
| parent | a4db087565dd2ecfa3bcc022277bed1a3c868fd3 (diff) | |
Passing some tactics to the new monad type.
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 2c153becf..20304b529 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -427,7 +427,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem (* replacing [res] with its value *) observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres))); (* Conclusion *) - observe_tac "exact" (fun g -> exact_check (app_constructor g) g) + observe_tac "exact" (fun g -> Proofview.V82.of_tactic (exact_check (app_constructor g)) g) ] ) g @@ -478,7 +478,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem observe_tac "principle" (Proofview.V82.of_tactic (assert_by (Name principle_id) princ_type - (Proofview.V82.tactic (exact_check f_principle)))); + (exact_check f_principle))); observe_tac "intro args_names" (tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) args_names); (* observe_tac "titi" (pose_proof (Name (Id.of_string "__")) (Reductionops.nf_beta Evd.empty ((mkApp (mkVar principle_id,Array.of_list bindings))))); *) observe_tac "idtac" tclIDTAC; |