diff options
| author | herbelin | 2006-10-19 07:46:03 +0000 |
|---|---|---|
| committer | herbelin | 2006-10-19 07:46:03 +0000 |
| commit | f5a8095075c8677efe5ee89b1d7ec53b1b10082b (patch) | |
| tree | 4c7acdb4c9001a9a55b0f117e2b3d8e5b7267621 | |
| parent | aef66d0112fd1ebebeaa8dd43721e91a4fce2305 (diff) | |
coqide: affichage des sous-buts et hypothèses et métas comme types de
telle sorte que les coercions vers sortclass ne soient pas affichées
(comme dans coqtop)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9249 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | ide/coq.ml | 6 | ||||
| -rw-r--r-- | parsing/printer.mli | 1 |
2 files changed, 4 insertions, 3 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index 3d489dcb54..4afb677d5c 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -261,7 +261,7 @@ type goal = hyp list * concl let prepare_hyp sigma env ((i,c,d) as a) = env, sigma, ((i,string_of_id i),c,d), - (msg (pr_var_decl env a), msg (pr_lconstr_env_at_top env d)) + (msg (pr_var_decl env a), msg (pr_ltype_env env d)) let prepare_hyps sigma env = assert (rel_context env = []); @@ -275,7 +275,7 @@ let prepare_hyps sigma env = let prepare_goal sigma g = let env = evar_env g in (prepare_hyps sigma env, - (env, sigma, g.evar_concl, msg (pr_lconstr_env_at_top env g.evar_concl))) + (env, sigma, g.evar_concl, msg (pr_ltype_env_at_top env g.evar_concl))) let prepare_hyps_filter info sigma env = assert (rel_context env = []); @@ -291,7 +291,7 @@ let prepare_hyps_filter info sigma env = let prepare_meta sigma env (m,typ) = env, sigma, - (msg (str " ?" ++ int m ++ str " : " ++ pr_lconstr_env_at_top env typ)) + (msg (str " ?" ++ int m ++ str " : " ++ pr_ltype_env_at_top env typ)) let prepare_metas info sigma env = List.fold_right diff --git a/parsing/printer.mli b/parsing/printer.mli index c63d7d71f0..dd2a7bad06 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -35,6 +35,7 @@ val pr_lconstr : constr -> std_ppcmds val pr_constr_env : env -> constr -> std_ppcmds val pr_constr : constr -> std_ppcmds +val pr_ltype_env_at_top : env -> types -> std_ppcmds val pr_ltype_env : env -> types -> std_ppcmds val pr_ltype : types -> std_ppcmds |