aboutsummaryrefslogtreecommitdiff
path: root/contrib/interface/showproof.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/interface/showproof.ml')
-rw-r--r--contrib/interface/showproof.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index e3f6572020..20c1cc04f5 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1202,7 +1202,7 @@ let rec natural_ntree ig ntree =
| TacExtend (_,"InductionIntro",[a]) ->
let id=(out_gen wit_ident a) in
natural_induction ig lh g gs ge id ltree true
- | TacApply (false,(c,_)) -> natural_apply ig lh g gs (snd c) ltree
+ | TacApply (_,false,(c,_)) -> natural_apply ig lh g gs (snd c) ltree
| TacExact c -> natural_exact ig lh g gs (snd c) ltree
| TacCut c -> natural_cut ig lh g gs (snd c) ltree
| TacExtend (_,"CutIntro",[a]) ->