diff options
Diffstat (limited to 'parsing/pptactic.ml')
| -rw-r--r-- | parsing/pptactic.ml | 25 |
1 files changed, 16 insertions, 9 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index b6c38cf93..d4fa5163e 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -133,6 +133,11 @@ let rec pr_message_token prid = function let pr_fresh_ids = prlist (fun s -> spc() ++ pr_or_var qs s) +let out_bindings = function + | ImplicitBindings l -> ImplicitBindings (List.map snd l) + | ExplicitBindings l -> ExplicitBindings (List.map (fun (loc,id,c) -> (loc,id,snd c)) l) + | NoBindings -> NoBindings + let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel Genarg.generic_argument) = match Genarg.genarg_tag x with | BoolArgType -> pr_arg str (if out_gen rawwit_bool x then "true" else "false") @@ -244,10 +249,12 @@ let rec pr_generic prc prlc prtac x = pr_arg (pr_red_expr (prc,prlc,pr_evaluable_reference)) (out_gen wit_red_expr x) | OpenConstrArgType b -> pr_arg prc (snd (out_gen (wit_open_constr_gen b) x)) - | ConstrWithBindingsArgType -> - pr_arg (pr_with_bindings prc prlc) (out_gen wit_constr_with_bindings x) + | ConstrWithBindingsArgType -> + let (c,b) = out_gen wit_constr_with_bindings x in + pr_arg (pr_with_bindings prc prlc) (c,out_bindings b) | BindingsArgType -> - pr_arg (pr_bindings_no_with prc prlc) (out_gen wit_bindings x) + pr_arg (pr_bindings_no_with prc prlc) + (out_bindings (out_gen wit_bindings x)) | List0ArgType _ -> hov 0 (fold_list0 (fun x a -> pr_generic prc prlc prtac x ++ a) x (mt())) | List1ArgType _ -> @@ -283,7 +290,7 @@ let pr_raw_extend prc prlc prtac = let pr_glob_extend prc prlc prtac = pr_extend_gen (pr_glob_generic prc prlc prtac) let pr_extend prc prlc prtac = - pr_extend_gen (pr_generic prc prlc prtac) + pr_extend_gen (pr_generic (fun c -> prc (Evd.empty,c)) (fun c -> prlc (Evd.empty,c)) prtac) (**********************************************************************) (* The tactic printer *) @@ -966,12 +973,12 @@ let strip_prod_binders_rawterm n (ty,_) = | _ -> error "Cannot translate fix tactic: not enough products" in strip_ty [] n ty -let strip_prod_binders_constr n ty = +let strip_prod_binders_constr n (sigma,ty) = let rec strip_ty acc n ty = - if n=0 then (List.rev acc, ty) else + if n=0 then (List.rev acc, (sigma,ty)) else match Term.kind_of_term ty with Term.Prod(na,a,b) -> - strip_ty (([dummy_loc,na],a)::acc) (n-1) b + strip_ty (([dummy_loc,na],(sigma,a))::acc) (n-1) b | _ -> error "Cannot translate fix tactic: not enough products" in strip_ty [] n ty @@ -1017,8 +1024,8 @@ and pr_glob_match_rule env t = let typed_printers = (pr_glob_tactic_level, - pr_constr_env, - pr_lconstr_env, + pr_open_constr_env, + pr_open_lconstr_env, pr_lconstr_pattern, pr_evaluable_reference_env, pr_inductive, |