diff options
| author | herbelin | 2003-09-12 14:41:05 +0000 |
|---|---|---|
| committer | herbelin | 2003-09-12 14:41:05 +0000 |
| commit | ae7e157abcb849a81433e042b06aacb59f0aee14 (patch) | |
| tree | 706abf4cc458304cfecdee34723ac97d7f1542e1 | |
| parent | fd8b1d101c07c69252719e9e35209baf019216be (diff) | |
Mise en place affichage spécifique pour le scope des types
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4361 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | translate/ppconstrnew.ml | 16 | ||||
| -rw-r--r-- | translate/ppconstrnew.mli | 2 |
2 files changed, 12 insertions, 6 deletions
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index e6385e3d33..087bcc90ac 100644 --- a/translate/ppconstrnew.ml +++ b/translate/ppconstrnew.ml @@ -522,11 +522,11 @@ let rec strip_context n iscast t = | RCast (_,c,_) -> strip_context n false c | _ -> anomaly "ppconstrnew: strip_context" -let transf env n iscast c = +let transf istype env n iscast c = if Options.do_translate() then let r = Constrintern.for_grammar - (Constrintern.interp_rawconstr_gen false Evd.empty env [] false + (Constrintern.interp_rawconstr_gen istype Evd.empty env [] false ([],[])) c in begin try @@ -534,16 +534,20 @@ let transf env n iscast c = let _ = Pretyping.understand_gen_tcc Evd.empty env [] None r in (*msgerrnl (str "Typage OK");*) () with e -> (*msgerrnl (str "Warning: can't type")*) () end; - Constrextern.extern_rawconstr (Termops.vars_of_env env) + (if istype then Constrextern.extern_rawtype + else Constrextern.extern_rawconstr) + (Termops.vars_of_env env) (strip_context n iscast r) else c -let pr_constr_env env c = pr lsimple (transf env 0 false c) -let pr_lconstr_env env c = pr ltop (transf env 0 false c) +let pr_constr_env env c = pr lsimple (transf false env 0 false c) +let pr_lconstr_env env c = pr ltop (transf false env 0 false c) let pr_constr c = pr_constr_env (Global.env()) c let pr_lconstr c = pr_lconstr_env (Global.env()) c -let pr_lconstr_env_n env n b c = pr ltop (transf env n b c) +let pr_lconstr_env_n env n b c = pr ltop (transf false env n b c) +let pr_type_env_n env n c = pr ltop (transf true env n false c) +let pr_type c = pr ltop (transf true (Global.env()) 0 false c) let pr_binders = pr_undelimited_binders pr_lconstr diff --git a/translate/ppconstrnew.mli b/translate/ppconstrnew.mli index 40b1225206..9b277cbd3f 100644 --- a/translate/ppconstrnew.mli +++ b/translate/ppconstrnew.mli @@ -52,6 +52,8 @@ val pr_lconstr : constr_expr -> std_ppcmds val pr_constr_env : env -> constr_expr -> std_ppcmds val pr_lconstr_env : env -> constr_expr -> std_ppcmds val pr_lconstr_env_n : env -> int -> bool -> constr_expr -> std_ppcmds +val pr_type_env_n : env -> int -> constr_expr -> std_ppcmds +val pr_type : constr_expr -> std_ppcmds val pr_cases_pattern : cases_pattern_expr -> std_ppcmds val pr_may_eval : ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> ('a,'b) may_eval |