diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-01 15:44:11 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-01 15:44:11 +0200 |
| commit | 84d49e38a245cbbbe5b6111a4e4d9afcbac2d33b (patch) | |
| tree | 0e6bff9cf7c2aaf6967352bd5b5f8c8a2831a570 /plugins/ltac | |
| parent | 48621da27d52be4825eea271d44bbd7362011dfa (diff) | |
| parent | 8ab00e5f272aa8f16d70a00323c57f2d4ef66f03 (diff) | |
Merge PR#561: Improving the Name API
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/tacentries.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/tacintern.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 6 |
4 files changed, 6 insertions, 6 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 4e254ea76..580c21d40 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -571,7 +571,7 @@ type 'a extra_genarg_printer = str "=>" ++ brk (1,4) ++ pr t)) | All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t - let pr_funvar n = spc () ++ pr_name n + let pr_funvar n = spc () ++ Name.print n let pr_let_clause k pr (id,(bl,t)) = hov 0 (keyword k ++ spc () ++ pr_lident id ++ prlist pr_funvar bl ++ diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 75f89a81e..f44ccbd3b 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -502,7 +502,7 @@ let print_ltacs () = | Tacexpr.TacFun (l, t) -> (l, t) | _ -> ([], body) in - let pr_ltac_fun_arg n = spc () ++ pr_name n in + let pr_ltac_fun_arg n = spc () ++ Name.print n in hov 2 (pr_qualid qid ++ prlist pr_ltac_fun_arg l) in Feedback.msg_notice (prlist_with_sep fnl pr_entry entries) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 2dc3bb378..0096abfa6 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -718,7 +718,7 @@ let split_ltac_fun = function | TacFun (l,t) -> (l,t) | t -> ([],t) -let pr_ltac_fun_arg n = spc () ++ pr_name n +let pr_ltac_fun_arg n = spc () ++ Name.print n let print_ltac id = try diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 6b0914ff9..594c4fa15 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1113,11 +1113,11 @@ let cons_and_check_name id l = let rec read_match_goal_hyps lfun ist env sigma lidh = function | (Hyp ((loc,na) as locna,mp))::tl -> - let lidh' = name_fold cons_and_check_name na lidh in + let lidh' = Name.fold_right cons_and_check_name na lidh in Hyp (locna,read_pattern lfun ist env sigma mp):: (read_match_goal_hyps lfun ist env sigma lidh' tl) | (Def ((loc,na) as locna,mv,mp))::tl -> - let lidh' = name_fold cons_and_check_name na lidh in + let lidh' = Name.fold_right cons_and_check_name na lidh in Def (locna,read_pattern lfun ist env sigma mv, read_pattern lfun ist env sigma mp):: (read_match_goal_hyps lfun ist env sigma lidh' tl) | [] -> [] @@ -1420,7 +1420,7 @@ and tactic_of_value ist vle = (str "A fully applied tactic is expected:" ++ spc() ++ Pp.str "missing " ++ Pp.str (String.plural numargs "argument") ++ Pp.str " for " ++ Pp.str (String.plural numargs "variable") ++ Pp.str " " ++ - pr_enum pr_name vars ++ Pp.str ".") + pr_enum Name.print vars ++ Pp.str ".") | VRec _ -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.") else if has_type vle (topwit wit_tactic) then let tac = out_gen (topwit wit_tactic) vle in |