diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-09 15:10:08 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-09 15:10:08 +0000 |
| commit | a4436a6a355ecb3fffb52d1ca3f2d983a5bcfefd (patch) | |
| tree | 0252d3bb7d7f9c55dad753f39e83de5efba41de4 /parsing/pretty.ml | |
| parent | f09ca438e24bc4016b4e778dd8fd4de4641b7636 (diff) | |
- constantes avec recettes
- discharge en deux temps, avec état remis comme au début de la section
(mais c'est toujours buggé)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@224 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/pretty.ml')
| -rw-r--r-- | parsing/pretty.ml | 17 |
1 files changed, 5 insertions, 12 deletions
diff --git a/parsing/pretty.ml b/parsing/pretty.ml index f12f5edec..848a2132e 100644 --- a/parsing/pretty.ml +++ b/parsing/pretty.ml @@ -49,7 +49,8 @@ let print_typed_value_in_env env (trm,typ) = let print_typed_value x = print_typed_value_in_env (Global.env ()) x let print_recipe = function - | Some c -> prterm c + | Some { contents = Cooked c } -> prterm c + | Some { contents = Recipe _ } -> [< 'sTR"<recipe>" >] | None -> [< 'sTR"<uncookable>" >] let fprint_recipe = function @@ -280,13 +281,7 @@ let rec print_library_entry with_values ent = match ent with | (sp,Lib.Leaf lobj) -> [< print_leaf_entry with_values sep (sp,lobj) >] - | (s,Lib.ClosedSection(_,ctxt)) -> - [< 'sTR"Closed Section " ; 'sTR (string_of_path s) ; 'fNL ; - if !print_closed_sections then - [< 'sTR " " ; hOV 0 [< print_context with_values ctxt >] >] - else - [< >] >] - | (_,Lib.OpenedSection str) -> + | (_,Lib.OpenedSection (str,_)) -> [< 'sTR(" >>>>>>> Section " ^ str) ; 'fNL >] | (_,Lib.FrozenState _) -> [< >] @@ -379,8 +374,7 @@ let crible (fn:string -> unit assumptions -> constr -> unit) name = crible_rec rest | _ -> crible_rec rest) - | (_, (Lib.OpenedSection _ | Lib.ClosedSection _ - | Lib.FrozenState _))::rest -> + | (_, (Lib.OpenedSection _ | Lib.FrozenState _))::rest -> crible_rec rest | [] -> () in @@ -396,7 +390,7 @@ let print_crible name = let read_sec_context sec = let rec get_cxt in_cxt = function - | ((sp,Lib.OpenedSection str) as hd)::rest -> + | ((sp,Lib.OpenedSection (str,_)) as hd)::rest -> if str = sec then (hd::in_cxt) else get_cxt (hd::in_cxt) rest | [] -> [] | hd::rest -> get_cxt (hd::in_cxt) rest @@ -495,7 +489,6 @@ let print_local_context () = [< print_last_const rest;print_mutual sp mib; 'fNL >] | "VARIABLE" -> [< >] | _ -> print_last_const rest) - | (sp,Lib.ClosedSection _)::rest -> print_last_const rest | _ -> [< >] in [< print_var_rec env; print_last_const env >] |