diff options
| author | herbelin | 2008-04-25 18:07:44 +0000 |
|---|---|---|
| committer | herbelin | 2008-04-25 18:07:44 +0000 |
| commit | 0cc6076e7d4d92c1d899d450b2336dadbeb5f1b1 (patch) | |
| tree | 388057bb70957e0b06431e57e3e248e47f4f0272 /parsing/tactic_printer.ml | |
| parent | a4bd836942106154703e10805405e8b4e6eb11ee (diff) | |
Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve
des théorèmes prouvés par récursion ou corécursion mutuelle.
Correction au passage du parsing et du printing des tactiques
fix/cofix et documentation de ces tactiques.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10850 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/tactic_printer.ml')
| -rw-r--r-- | parsing/tactic_printer.ml | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml index 91c1bc0c4f..11b755fa03 100644 --- a/parsing/tactic_printer.ml +++ b/parsing/tactic_printer.ml @@ -34,7 +34,7 @@ let pr_rule = function | Nested(cmpd,_) -> begin match cmpd with - Tactic (texp,_) -> hov 0 (pr_tactic texp) + | Tactic (texp,_) -> hov 0 (pr_tactic texp) | Proof_instr (_,instr) -> hov 0 (pr_proof_instr instr) end | Daimon -> str "<Daimon>" @@ -50,6 +50,14 @@ let pr_rule_dot = function | r -> pr_rule r ++ if uses_default_tac r then str "..." else str"." +let pr_rule_dot_fnl = function + | Nested (Tactic (TacAtom (_,(TacMutualFix (true,_,_,_) + | TacMutualCofix (true,_,_))),_),_) -> + (* Very big hack to not display hidden tactics in "Theorem with" *) + (* (would not scale!) *) + mt () + | r -> pr_rule_dot r ++ fnl () + exception Different (* We remove from the var context of env what is already in osign *) @@ -155,7 +163,7 @@ let rec print_script nochange sigma pf = (print_script nochange sigma) spfl ) | Some(rule,spfl) -> ((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++ - pr_rule_dot rule ++ fnl () ++ + pr_rule_dot_fnl rule ++ prlist_with_sep pr_fnl (print_script nochange sigma) spfl ) @@ -189,7 +197,7 @@ let print_treescript nochange sigma pf = | Some(r,spfl) -> let indent = if List.length spfl >= 2 then 1 else 0 in (if nochange then mt () else (pr_change pf.goal ++ fnl ())) ++ - hv indent (pr_rule_dot r ++ fnl () ++ prlist_with_sep fnl aux spfl) + hv indent (pr_rule_dot_fnl r ++ prlist_with_sep fnl aux spfl) in hov 0 (aux pf) let rec print_info_script sigma osign pf = |