diff options
| author | Pierre-Marie Pédrot | 2015-05-05 00:20:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-05-05 00:20:54 +0200 |
| commit | 34e6a7149a69791cc736bdd9b2b909be9f21ec8f (patch) | |
| tree | f33a4ed37d7fff96df7a720fe6146ecce56aba81 /parsing | |
| parent | 72644c7f7b3f0fcc56779acfcfa4bfc9f041ebde (diff) | |
| parent | df54c829a4c06a93de47df4e8ccc441721360da8 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.ml4 | 10 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 1 | ||||
| -rw-r--r-- | parsing/g_xml.ml4 | 2 |
3 files changed, 4 insertions, 9 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 3bb029a888..74f17f9fb6 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -223,12 +223,6 @@ GEXTEND Gram CHole (!@loc, None, IntroAnonymous, Some arg) ] ] ; - forall: - [ [ "forall" -> () ] ] - ; - lambda: - [ [ "fun" -> () ] ] - ; record_declaration: [ [ fs = LIST0 record_field_declaration SEP ";" -> CRecord (!@loc, None, fs) (* | c = lconstr; "with"; fs = LIST1 record_field_declaration SEP ";" -> *) @@ -240,9 +234,9 @@ GEXTEND Gram (id, abstract_constr_expr c (binders_of_lidents params)) ] ] ; binder_constr: - [ [ forall; bl = open_binders; ","; c = operconstr LEVEL "200" -> + [ [ "forall"; bl = open_binders; ","; c = operconstr LEVEL "200" -> mkCProdN (!@loc) bl c - | lambda; bl = open_binders; "=>"; c = operconstr LEVEL "200" -> + | "fun"; bl = open_binders; "=>"; c = operconstr LEVEL "200" -> mkCLambdaN (!@loc) bl c | "let"; id=name; bl = binders; ty = type_cstr; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index cf7f6af28b..09059b410e 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -79,6 +79,7 @@ GEXTEND Gram GLOBAL: vernac gallina_ext tactic_mode noedit_mode subprf subgoal_command; vernac: FIRST [ [ IDENT "Time"; l = vernac_list -> VernacTime l + | IDENT "Redirect"; s = ne_string; l = vernac_list -> VernacRedirect (s, l) | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v) | IDENT "Fail"; v = vernac -> VernacFail v diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 84e4a5732e..992f9c59af 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -58,7 +58,7 @@ END let error_bad_arity loc n = let s = match n with 0 -> "none" | 1 -> "one" | 2 -> "two" | _ -> "many" in - user_err_loc (loc,"",str ("wrong number of arguments (expect "^s^").")) + user_err_loc (loc,"",str "wrong number of arguments (expect " ++ str s ++ str ").") (* Interpreting attributes *) |