aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--parsing/g_ltac.ml47
-rw-r--r--parsing/g_ltacnew.ml48
-rw-r--r--translate/ppconstrnew.ml11
-rw-r--r--translate/pptacticnew.ml15
4 files changed, 25 insertions, 16 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 5c74f4ef6..fb3850c90 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -96,8 +96,7 @@ GEXTEND Gram
| pc = Constr.constr_pattern -> Term pc ] ]
;
match_hyps:
- [ [ id = identref; ":"; mp = match_pattern -> Hyp (id, mp)
- | IDENT "_"; ":"; mp = match_pattern -> NoHypId mp ] ]
+ [ [ na = name; ":"; mp = match_pattern -> Hyp (na, mp) ] ]
;
match_context_rule:
[ [ "["; largs = LIST0 match_hyps SEP ";"; "|-"; mp = match_pattern; "]";
@@ -146,8 +145,8 @@ GEXTEND Gram
| IDENT "Rec"; rc = rec_clause ->
warning "'Rec f ...' is obsolete; use 'Rec f ... In f' instead";
TacLetRecIn ([rc],TacArg (Reference (Libnames.Ident (fst rc))))
- | IDENT "Rec"; rcl = LIST1 rec_clause SEP "And"; IDENT "In";
- body = tactic_expr -> TacLetRecIn (rcl,body)
+ | IDENT "Rec"; rc = rec_clause; rcl = LIST0 rec_clause SEP "And";
+ [IDENT "In" | "in"]; body = tactic_expr -> TacLetRecIn (rc::rcl,body)
| IDENT "Let"; llc = LIST1 let_clause SEP "And"; IDENT "In";
u = tactic_expr -> TacLetIn (make_letin_clause loc llc,u)
(* Let cas LetCut est subsumé par "Assert id := c" tandis que le cas
diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4
index b364bb874..834e978e4 100644
--- a/parsing/g_ltacnew.ml4
+++ b/parsing/g_ltacnew.ml4
@@ -89,7 +89,7 @@ GEXTEND Gram
| "1" RIGHTA
[ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr ->
TacFun (it,body)
- | IDENT "rec"; rcl = LIST1 rec_clause SEP "with"; "in";
+ | "let"; IDENT "rec"; rcl = LIST1 rec_clause SEP "with"; "in";
body = tactic_expr -> TacLetRecIn (rcl,body)
| "let"; llc = LIST1 let_clause SEP "with"; "in";
u = tactic_expr -> TacLetIn (make_letin_clause loc llc,u)
@@ -136,7 +136,6 @@ GEXTEND Gram
tactic_atom:
[ [ id = METAIDENT -> MetaIdArg (loc,id)
| r = reference -> Reference r
- | "?"; n = natural -> ConstrMayEval (ConstrTerm (CPatVar (loc,(false,Pattern.patvar_of_int n))))
| "()" -> TacVoid ] ]
;
input_fun:
@@ -154,7 +153,7 @@ GEXTEND Gram
LETTOPCLAUSE (id, c) ] ]
;
rec_clause:
- [ [ name = identref; it = LIST1 input_fun; "=>"; body = tactic_expr ->
+ [ [ name = identref; it = LIST1 input_fun; ":="; body = tactic_expr ->
(name,(it,body)) ] ]
;
match_pattern:
@@ -164,8 +163,7 @@ GEXTEND Gram
| pc = Constr.constr_pattern -> Term pc ] ]
;
match_hyps:
- [ [ id = identref; ":"; mp = match_pattern -> Hyp (id, mp)
- | IDENT "_"; ":"; mp = match_pattern -> NoHypId mp ] ]
+ [ [ na = name; ":"; mp = match_pattern -> Hyp (na, mp) ] ]
;
match_context_rule:
[ [ "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; "]";
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 92feaa7de..a3b430c7d 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -527,6 +527,16 @@ let pr_lconstr_env env c = pr ltop (transf env c)
let pr_constr c = pr_constr_env (Global.env()) c
let pr_lconstr c = pr_lconstr_env (Global.env()) c
+let transf_pattern env c =
+ if Options.do_translate() then
+ Constrextern.extern_rawconstr (Termops.vars_of_env env)
+ (Constrintern.for_grammar
+ (Constrintern.interp_rawconstr_gen false Evd.empty env [] None ([],[]))
+ c)
+ else c
+
+let pr_pattern c = pr lsimple (transf_pattern (Global.env()) c)
+
let pr_rawconstr_env env c =
pr_constr (Constrextern.extern_rawconstr (Termops.vars_of_env env) c)
let pr_lrawconstr_env env c =
@@ -547,7 +557,6 @@ let pr_binders l =
let pr_cases_pattern = pr_patt ltop
-let pr_pattern = pr_constr
let pr_occurrences prc (nl,c) =
prlist (fun n -> int n ++ spc ()) nl ++
str"(" ++ prc c ++ str")"
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 3f268fe69..67d6638a0 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -39,6 +39,10 @@ let pr_quantified_hypothesis = function
let pr_quantified_hypothesis_arg h = spc () ++ pr_quantified_hypothesis h
+let pr_or_metanum pr = function
+ | AN x -> pr x
+ | MetaNum (_,n) -> Pattern.pr_patvar n
+
(*
let pr_binding prc = function
| NamedHyp id, c -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c)
@@ -108,8 +112,7 @@ let pr_match_pattern pr_pat = function
| Subterm (Some id,a) -> pr_id id ++ str "[" ++ pr_pat a ++ str "]"
let pr_match_hyps pr_pat = function
- | NoHypId mp -> str "_:" ++ pr_match_pattern pr_pat mp
- | Hyp ((_,id),mp) -> pr_id id ++ str ":" ++ pr_match_pattern pr_pat mp
+ | Hyp ((_,na),mp) -> pr_name na ++ str ":" ++ pr_match_pattern pr_pat mp
let pr_match_rule m pr pr_pat = function
| Pat ([],mp,t) when m ->
@@ -137,15 +140,15 @@ let pr_let_clause k pr prc pr_cst = function
let pr_let_clauses pr prc pr_cst = function
| hd::tl ->
hv 0
- (pr_let_clause "let " pr prc pr_cst hd ++ spc () ++
- prlist_with_sep spc (pr_let_clause "with " pr prc pr_cst) tl)
+ (pr_let_clause "let " pr prc pr_cst hd ++
+ prlist (fun t -> spc () ++ pr_let_clause "with " pr prc pr_cst t) tl)
| [] -> anomaly "LetIn must declare at least one binding"
let pr_rec_clause pr ((_,id),(l,t)) =
- pr_id id ++ prlist pr_funvar l ++ str "=>" ++ spc () ++ pr t
+ hov 0 (pr_id id ++ prlist pr_funvar l ++ str " :=") ++ spc () ++ pr t
let pr_rec_clauses pr l =
- prlist_with_sep (fun () -> fnl () ++ str "and ") (pr_rec_clause pr) l
+ prlist_with_sep (fun () -> fnl () ++ str "with ") (pr_rec_clause pr) l
let pr_hintbases = function
| None -> spc () ++ str "with *"
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 03:46:31 +0000