diff options
| author | Pierre-Marie Pédrot | 2013-12-01 18:47:55 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2013-12-01 18:55:11 +0100 |
| commit | cb290d81c46ec370e303e1414e203c40c8fa1174 (patch) | |
| tree | 8f48d26fe7f68a905c2194239523c91316dc0139 /printing/pptactic.ml | |
| parent | 233a782a2336f003869f82e697a567ed02885f23 (diff) | |
Removing RefArgType generic argument.
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index f091a2e1dd..77f5db3b4c 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -148,7 +148,6 @@ let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generi | IntOrVarArgType -> pr_or_var int (out_gen (rawwit wit_int_or_var) x) | IdentArgType b -> if_pattern_ident b pr_id (out_gen (rawwit wit_ident) x) | VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x) - | RefArgType -> prref (out_gen (rawwit wit_ref) x) | GenArgType -> pr_raw_generic prc prlc prtac prpat prref (out_gen (rawwit wit_genarg) x) | ConstrArgType -> prc (out_gen (rawwit wit_constr) x) | ConstrMayEvalArgType -> @@ -183,7 +182,6 @@ let rec pr_glb_generic prc prlc prtac prpat x = | IntOrVarArgType -> pr_or_var int (out_gen (glbwit wit_int_or_var) x) | IdentArgType b -> if_pattern_ident b pr_id (out_gen (glbwit wit_ident) x) | VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x) - | RefArgType -> pr_or_var (pr_located pr_global) (out_gen (glbwit wit_ref) x) | GenArgType -> pr_glb_generic prc prlc prtac prpat (out_gen (glbwit wit_genarg) x) | ConstrArgType -> prc (out_gen (glbwit wit_constr) x) | ConstrMayEvalArgType -> @@ -219,7 +217,6 @@ let rec pr_top_generic prc prlc prtac prpat x = | IntOrVarArgType -> pr_or_var int (out_gen (topwit wit_int_or_var) x) | IdentArgType b -> if_pattern_ident b pr_id (out_gen (topwit wit_ident) x) | VarArgType -> pr_id (out_gen (topwit wit_var) x) - | RefArgType -> pr_global (out_gen (topwit wit_ref) x) | GenArgType -> pr_top_generic prc prlc prtac prpat (out_gen (topwit wit_genarg) x) | ConstrArgType -> prc (out_gen (topwit wit_constr) x) | ConstrMayEvalArgType -> prc (out_gen (topwit wit_constr_may_eval) x) @@ -1032,6 +1029,8 @@ let register_uniform_printer wit pr = Genprint.register_print0 wit pr pr pr let () = + Genprint.register_print0 Constrarg.wit_ref + pr_reference (pr_or_var (pr_located pr_global)) pr_global; Genprint.register_print0 Constrarg.wit_intro_pattern pr_intro_pattern pr_intro_pattern pr_intro_pattern; Genprint.register_print0 Constrarg.wit_sort |