diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-28 02:08:42 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-28 02:18:25 +0100 |
| commit | cb2f6a95ee72edb956f419a24f8385c8ae7f96f4 (patch) | |
| tree | 2ddf7103c75e4e824d5bfefade3ec774498fc131 /printing | |
| parent | 28d4740736e5ef3b6f8547710dcf7e5b4d11cabd (diff) | |
Removing the special status of open_constr generic argument.
We also intepret it at toplevel as a true constr and push the resulting
evarmap in the current state.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/pptactic.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index b98738ce3..6e051a1fc 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -270,7 +270,6 @@ module Make | IdentArgType -> pr_id (out_gen (rawwit wit_ident) x) | VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x) | ConstrArgType -> prc (out_gen (rawwit wit_constr) x) - | OpenConstrArgType -> prc (snd (out_gen (rawwit wit_open_constr) x)) | ListArgType _ -> let list_unpacker wit l = let map x = pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) in @@ -301,7 +300,6 @@ module Make | IdentArgType -> pr_id (out_gen (glbwit wit_ident) x) | VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x) | ConstrArgType -> prc (out_gen (glbwit wit_constr) x) - | OpenConstrArgType -> prc (snd (out_gen (glbwit wit_open_constr) x)) | ListArgType _ -> let list_unpacker wit l = let map x = pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x) in @@ -331,7 +329,6 @@ module Make | IdentArgType -> pr_id (out_gen (topwit wit_ident) x) | VarArgType -> pr_id (out_gen (topwit wit_var) x) | ConstrArgType -> prc (out_gen (topwit wit_constr) x) - | OpenConstrArgType -> prc (snd (out_gen (topwit wit_open_constr) x)) | ListArgType _ -> let list_unpacker wit l = let map x = pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) in @@ -1425,6 +1422,12 @@ let () = (fun (c,_) -> Printer.pr_glob_constr c) Printer.pr_closed_glob ; + Genprint.register_print0 + Constrarg.wit_open_constr + Ppconstr.pr_constr_expr + (fun (c, _) -> Printer.pr_glob_constr c) + Printer.pr_constr + ; Genprint.register_print0 Constrarg.wit_red_expr (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr)) (pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr)) |