diff options
author | Julien Forest <julien.forest@ensiie.fr> | 2014-04-14 23:22:14 +0200 |
---|---|---|
committer | Julien Forest <julien.forest@ensiie.fr> | 2014-04-14 23:22:14 +0200 |
commit | 5fb2050e424062540ffbf22de0838fafe4de0a41 (patch) | |
tree | 235a18a0481828d9af31c28df41e3492c5adb044 /tactics/extraargs.ml4 | |
parent | a51d94e77bd352522744da4dbdbf98b36c19631e (diff) |
Closing bug #3260
adding a new grammar entry for clauses
Diffstat (limited to 'tactics/extraargs.ml4')
-rw-r--r-- | tactics/extraargs.ml4 | 88 |
1 files changed, 0 insertions, 88 deletions
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index c156e869d..dc41cf8e3 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -208,94 +208,6 @@ END let pr_by_arg_tac prtac opt_c = pr_by_arg_tac () () prtac opt_c -let pr_in_hyp pr_id (lo,concl) : Pp.std_ppcmds = - match lo,concl with - | Some [],true -> mt () - | None,true -> str "in" ++ spc () ++ str "*" - | None,false -> str "in" ++ spc () ++ str "*" ++ spc () ++ str "|-" - | Some l,_ -> - str "in" ++ - spc () ++ prlist_with_sep pr_comma pr_id l ++ - match concl with - | true -> spc () ++ str "|-" ++ spc () ++ str "*" - | _ -> mt () - - -let pr_in_arg_hyp _ _ _ = pr_in_hyp (fun (_,id) -> Ppconstr.pr_id id) - -let pr_in_arg_hyp_typed _ _ _ = pr_in_hyp Ppconstr.pr_id - - -let pr_var_list_gen pr_id = Pp.prlist_with_sep (fun () -> str ",") pr_id - -let pr_var_list_typed _ _ _ = pr_var_list_gen Ppconstr.pr_id - -let pr_var_list _ _ _ = pr_var_list_gen (fun (_,id) -> Ppconstr.pr_id id) - - -ARGUMENT EXTEND comma_var_lne - PRINTED BY pr_var_list_typed - RAW_TYPED AS var list - RAW_PRINTED BY pr_var_list - GLOB_TYPED AS var list - GLOB_PRINTED BY pr_var_list -| [ var(x) ] -> [ [x] ] -| [ var(x) "," comma_var_lne(l) ] -> [x::l] -END - -ARGUMENT EXTEND comma_var_l - PRINTED BY pr_var_list_typed - RAW_TYPED AS var list - RAW_PRINTED BY pr_var_list - GLOB_TYPED AS var list - GLOB_PRINTED BY pr_var_list -| [ comma_var_lne(l) ] -> [l] -| [] -> [ [] ] -END - -let pr_in_concl _ _ _ = function true -> str "|- " ++ spc () ++ str "*" | _ -> str "|-" - -ARGUMENT EXTEND inconcl - TYPED AS bool - PRINTED BY pr_in_concl -| [ "|-" "*" ] -> [ true ] -| [ "|-" ] -> [ false ] -END - - - -ARGUMENT EXTEND in_arg_hyp - PRINTED BY pr_in_arg_hyp_typed - RAW_TYPED AS var list option * bool - RAW_PRINTED BY pr_in_arg_hyp - GLOB_TYPED AS var list option * bool - GLOB_PRINTED BY pr_in_arg_hyp -| [ "in" "*" ] -> [(None,true)] -| [ "in" "*" inconcl_opt(b) ] -> [let onconcl = match b with Some b -> b | None -> true in (None,onconcl)] -| [ "in" comma_var_l(l) inconcl_opt(b) ] -> [ let onconcl = match b with Some b -> b | None -> false in - Some l, onconcl - ] -| [ ] -> [ (Some [],true) ] -END - -let pr_in_arg_hyp = pr_in_arg_hyp_typed () () () - -let gen_in_arg_hyp_to_clause trad_id (hyps ,concl) : clause = - {onhyps= - Option.map - (fun l -> - List.map - (fun id -> ( (AllOccurrences,trad_id id),InHyp)) - l - ) - hyps; - concl_occs = if concl then AllOccurrences else NoOccurrences} - - -let raw_in_arg_hyp_to_clause = gen_in_arg_hyp_to_clause snd -let glob_in_arg_hyp_to_clause = gen_in_arg_hyp_to_clause (fun x -> x) - - (* spiwack argument for the commands of the retroknowledge *) let wit_r_nat_field = |