diff options
| author | Hugo Herbelin | 2014-08-14 20:44:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-08-18 18:56:38 +0200 |
| commit | d5fece25d8964d5d9fcd55b66164286aeef5fb9f (patch) | |
| tree | 60d584831ef3574c8d07daaef85929bd81a12d88 /plugins/funind/invfun.ml | |
| parent | 4684ae383a6ee56b4717026479eceb3b41b45ab0 (diff) | |
Reorganization of tactics:
- made "apply" tactics of type Proofview.tactic, as well as other inner
functions about elim and assert
- used same hypothesis naming policy for intros and internal_cut (towards a
reorganization of intro patterns)
- "apply ... in H as pat" now supports any kind of introduction
pattern (doc not changed)
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 5682c2aa47..4fcc65bda9 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -487,7 +487,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem (fun gl -> let term = mkApp (mkVar principle_id,Array.of_list bindings) in let gl', _ty = pf_eapply Typing.e_type_of gl term in - apply term gl') + Proofview.V82.of_tactic (apply term) gl') )) (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g ) ] |