diff options
| author | gregoire | 2005-12-02 10:01:15 +0000 |
|---|---|---|
| committer | gregoire | 2005-12-02 10:01:15 +0000 |
| commit | bf578ad5e2f63b7a36aeaef5e0597101db1bd24a (patch) | |
| tree | c0bc4e5f9ae67b8a03b28134dab3dcfe31d184dd /parsing/tactic_printer.ml | |
| parent | 825a338a1ddf1685d55bb5193aa5da078a534e1c (diff) | |
Changement des named_context
Ajout de cast indiquant au kernel la strategie a suivre
Resolution du bug sur les coinductifs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/tactic_printer.ml')
| -rw-r--r-- | parsing/tactic_printer.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml index 942bce7987..6b5b35dd2a 100644 --- a/parsing/tactic_printer.ml +++ b/parsing/tactic_printer.ml @@ -53,12 +53,13 @@ let thin_sign osign sign = try if Sign.lookup_named id osign = (id,c,ty) then sign else raise Different - with Not_found | Different -> add_named_decl d sign) - sign ~init:empty_named_context + with Not_found | Different -> Environ.push_named_context_val d sign) + sign ~init:Environ.empty_named_context_val let rec print_proof sigma osign pf = let {evar_hyps=hyps; evar_concl=cl; evar_body=body} = pf.goal in + let hyps = Environ.named_context_of_val hyps in let hyps' = thin_sign osign hyps in match pf.ref with | None -> @@ -78,6 +79,7 @@ let pr_change gl = let rec print_script nochange sigma osign pf = let {evar_hyps=sign; evar_concl=cl} = pf.goal in + let sign = Environ.named_context_of_val sign in match pf.ref with | None -> (if nochange then @@ -124,10 +126,12 @@ let rec print_info_script sigma osign pf = (str "." ++ fnl ()) else (str";" ++ brk(1,3) ++ - print_info_script sigma sign pf1) + print_info_script sigma + (Environ.named_context_of_val sign) pf1) | _ -> (str"." ++ fnl () ++ prlist_with_sep pr_fnl - (print_info_script sigma sign) spfl)) + (print_info_script sigma + (Environ.named_context_of_val sign)) spfl)) let format_print_info_script sigma osign pf = hov 0 (print_info_script sigma osign pf) |