diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-16 15:24:56 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-16 16:02:48 +0200 |
| commit | 6aac2c78ad5dec79c6ed16a50accde57c37398a9 (patch) | |
| tree | 53968b5035fd9b70d4431130cf12621f314cb187 /ltac/tacinterp.ml | |
| parent | a452e436af72ccc1b8342ac6b666f0ff202cc20a (diff) | |
| parent | 791f3254cba602672b834ec3484d308db074b684 (diff) | |
Merge 'pr/191' into trunk
Diffstat (limited to 'ltac/tacinterp.ml')
| -rw-r--r-- | ltac/tacinterp.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 649764da3..3716de251 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1256,6 +1256,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with strbrk "There is an \"Info\" command to replace it." ++fnl () ++ strbrk "Some specific verbose tactics may also exist, such as info_eauto."); eval_tactic ist tac + | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac) (* For extensions *) | TacAlias (loc,s,l) -> let (ids, body) = Tacenv.interp_alias s in |