diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-14 20:44:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-18 18:56:38 +0200 |
| commit | d5fece25d8964d5d9fcd55b66164286aeef5fb9f (patch) | |
| tree | 60d584831ef3574c8d07daaef85929bd81a12d88 /plugins/cc | |
| 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/cc')
| -rw-r--r-- | plugins/cc/cctac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 70aaa0c0f..3151a7ec7 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -486,7 +486,7 @@ let f_equal = else Tacticals.New.tclTRY (Tacticals.New.tclTHEN ((new_app_global _eq [|ty; c1; c2|]) Tactics.cut) - (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) (fun c -> Proofview.V82.tactic (apply c))))) + (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply))) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e in Proofview.tclORELSE |