diff options
| author | corbinea | 2007-01-25 17:54:01 +0000 |
|---|---|---|
| committer | corbinea | 2007-01-25 17:54:01 +0000 |
| commit | 25f472a9b7a5b9638357924aca635b5cc82b66f4 (patch) | |
| tree | 4258bb1a2c60b4d6b974813a20abc16ece9af31f /parsing/printer.ml | |
| parent | 6e50e71e8ab3e501ec22b6d49cece3f6464e38d2 (diff) | |
decl mode: anonymous facts
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9534 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/printer.ml')
| -rw-r--r-- | parsing/printer.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index dd8264ea77..c1a4415e32 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -262,9 +262,9 @@ let default_pr_goal g = pr_context_of env, pr_ltype_env_at_top env g.evar_concl else - let {pm_subgoals=metas;pm_hyps=among} = get_info g in + let {pm_subgoals=metas} = get_info g in (str " *** Declarative Mode ***" ++ fnl ()++fnl ()), - pr_restricted_named_context among env, + pr_context_of env, pr_subgoal_metas metas env in preamb ++ |