diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_ltac.ml4 | 24 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 33 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 7 |
3 files changed, 16 insertions, 48 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 79e88f8cd..87d45dc56 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -20,19 +20,8 @@ open Pcoq open Prim open Tactic -type let_clause_kind = - | LETTOPCLAUSE of Names.identifier * constr_expr - | LETCLAUSE of - (Names.identifier Util.located * raw_tactic_expr option * raw_tactic_arg) - let fail_default_value = ArgArg 0 -let out_letin_clause loc = function - | LETTOPCLAUSE _ -> user_err_loc (loc, "", (str "Syntax Error")) - | LETCLAUSE (id,c,d) -> (id,c,d) - -let make_letin_clause loc = List.map (out_letin_clause loc) - let arg_of_expr = function TacArg a -> a | e -> Tacexp (e:raw_tactic_expr) @@ -122,10 +111,9 @@ GEXTEND Gram [ RIGHTA [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr LEVEL "5" -> TacFun (it,body) - | "let"; IDENT "rec"; rcl = LIST1 rec_clause SEP "with"; "in"; - body = tactic_expr LEVEL "5" -> TacLetRecIn (rcl,body) - | "let"; llc = LIST1 let_clause SEP "with"; "in"; - u = tactic_expr LEVEL "5" -> TacLetIn (make_letin_clause loc llc,u) + | "let"; isrec = [IDENT "rec" -> true | -> false]; + llc = LIST1 let_clause SEP "with"; "in"; + body = tactic_expr LEVEL "5" -> TacLetIn (isrec,llc,body) | IDENT "info"; tc = tactic_expr LEVEL "5" -> TacInfo tc ] ] ; (* Tactic arguments *) @@ -173,12 +161,12 @@ GEXTEND Gram ; let_clause: [ [ id = identref; ":="; te = tactic_expr -> - LETCLAUSE (id, None, arg_of_expr te) + (id, arg_of_expr te) | id = identref; args = LIST1 input_fun; ":="; te = tactic_expr -> - LETCLAUSE (id, None, arg_of_expr (TacFun(args,te))) ] ] + (id, arg_of_expr (TacFun(args,te))) ] ] ; rec_clause: - [ [ name = identref; it = LIST1 input_fun; ":="; body = tactic_expr -> + [ [ name = identref; it = LIST0 input_fun; ":="; body = tactic_expr -> (name,(it,body)) ] ] ; match_pattern: diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 7d83cffb6..67858b3c6 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -473,29 +473,16 @@ let pr_funvar = function | None -> spc () ++ str "_" | Some id -> spc () ++ pr_id id -let pr_let_clause k pr = function - | (id,None,t) -> - hov 0 (str k ++ pr_lident id ++ str " :=" ++ brk (1,1) ++ - pr (TacArg t)) - | (id,Some c,t) -> - hv 0 (str k ++ pr_lident id ++ str" :" ++ brk(1,2) ++ - pr c ++ - str " :=" ++ brk (1,1) ++ pr (TacArg t)) - -let pr_let_clauses pr = function +let pr_let_clause k pr (id,t) = + hov 0 (str k ++ pr_lident id ++ str " :=" ++ brk (1,1) ++ pr (TacArg t)) + +let pr_let_clauses recflag pr = function | hd::tl -> hv 0 - (pr_let_clause "let " pr hd ++ + (pr_let_clause (if recflag then "let rec " else "let ") pr hd ++ prlist (fun t -> spc () ++ pr_let_clause "with " pr t) tl) | [] -> anomaly "LetIn must declare at least one binding" -let pr_rec_clause pr (id,(l,t)) = - hov 0 - (pr_lident id ++ prlist pr_funvar l ++ str " :=") ++ spc () ++ pr t - -let pr_rec_clauses pr l = - prlist_with_sep (fun () -> fnl () ++ str "with ") (pr_rec_clause pr) l - let pr_seq_body pr tl = hv 0 (str "[ " ++ prlist_with_sep (fun () -> spc () ++ str "| ") pr tl ++ @@ -858,15 +845,9 @@ let rec pr_tac inherited tac = (str "abstract (" ++ pr_tac (labstract,L) t ++ str")" ++ spc () ++ str "using " ++ pr_id s), labstract - | TacLetRecIn (l,t) -> - hv 0 - (str "let rec " ++ pr_rec_clauses (pr_tac ltop) l ++ str " in" ++ - fnl () ++ pr_tac (llet,E) t), - llet - | TacLetIn (llc,u) -> + | TacLetIn (recflag,llc,u) -> v 0 - (hv 0 (pr_let_clauses (pr_tac ltop) llc - ++ str " in") ++ + (hv 0 (pr_let_clauses recflag (pr_tac ltop) llc ++ str " in") ++ fnl () ++ pr_tac (llet,E) u), llet | TacMatch (lz,t,lrul) -> diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 26dff3927..b5ad753af 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -448,13 +448,12 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function | Tacexpr.TacRec (id,(idl,t)) -> TacRec (loc,(id,(idl,f t))) | Tacexpr.TacRecIn (l,t) -> TacRecIn(loc,List.map (fun (id,t) -> (id,f t)) l,f t) *) - | Tacexpr.TacLetIn (l,t) -> + | Tacexpr.TacLetIn (isrec,l,t) -> let f = - mlexpr_of_triple + mlexpr_of_pair (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_ident) - (mlexpr_of_option mlexpr_of_tactic) mlexpr_of_tactic_arg in - <:expr< Tacexpr.TacLetIn $mlexpr_of_list f l$ $mlexpr_of_tactic t$ >> + <:expr< Tacexpr.TacLetIn $mlexpr_of_bool isrec$ $mlexpr_of_list f l$ $mlexpr_of_tactic t$ >> | Tacexpr.TacMatch (lz,t,l) -> <:expr< Tacexpr.TacMatch $mlexpr_of_bool lz$ |