diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/ppconstr.ml | 1 | ||||
| -rw-r--r-- | parsing/ppconstr.mli | 1 | ||||
| -rw-r--r-- | parsing/printer.ml | 13 | ||||
| -rw-r--r-- | parsing/printer.mli | 6 |
4 files changed, 21 insertions, 0 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 597505686d..cf5a58eea4 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -122,6 +122,7 @@ let pr_rawsort = function let pr_id = pr_id let pr_name = pr_name let pr_qualid = pr_qualid +let pr_patvar = pr_id let pr_expl_args pr (a,expl) = match expl with diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli index 2becdbcfd6..afa744a507 100644 --- a/parsing/ppconstr.mli +++ b/parsing/ppconstr.mli @@ -46,6 +46,7 @@ val pr_sep_com : val pr_id : identifier -> std_ppcmds val pr_name : name -> std_ppcmds val pr_qualid : qualid -> std_ppcmds +val pr_patvar : patvar -> std_ppcmds val pr_with_occurrences : ('a -> std_ppcmds) -> 'a with_occurrences -> std_ppcmds diff --git a/parsing/printer.ml b/parsing/printer.ml index d3c4ae63da..61f7e377a2 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -57,6 +57,19 @@ let pr_constr t = pr_constr_env (Global.env()) t let pr_open_lconstr (_,c) = pr_lconstr c let pr_open_constr (_,c) = pr_constr c +let pr_constr_under_binders_env_gen pr env (ids,c) = + (* Warning: clashes can occur with variables of same name in env but *) + (* we also need to preserve the actual names of the patterns *) + (* So what to do? *) + let assums = List.map (fun id -> (Name id,(* dummy *) mkProp)) ids in + pr (push_rels_assum assums env) c + +let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_constr_env +let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_lconstr_env + +let pr_constr_under_binders c = pr_constr_under_binders_env (Global.env()) c +let pr_lconstr_under_binders c = pr_lconstr_under_binders_env (Global.env()) c + let pr_type_core at_top env t = pr_constr_expr (extern_type at_top env t) let pr_ltype_core at_top env t = diff --git a/parsing/printer.mli b/parsing/printer.mli index 52a0900759..241650b7d6 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -38,6 +38,12 @@ val pr_open_constr : open_constr -> std_ppcmds val pr_open_lconstr_env : env -> open_constr -> std_ppcmds val pr_open_lconstr : open_constr -> std_ppcmds +val pr_constr_under_binders_env : env -> constr_under_binders -> std_ppcmds +val pr_constr_under_binders : constr_under_binders -> std_ppcmds + +val pr_lconstr_under_binders_env : env -> constr_under_binders -> std_ppcmds +val pr_lconstr_under_binders : constr_under_binders -> 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 |