From 164c6861860e6b52818c031f901ffeff91fca16a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 26 Jan 2016 16:56:33 +0100 Subject: Imported Upstream version 8.5 --- parsing/compat.ml4 | 2 +- parsing/egramcoq.ml | 2 +- parsing/egramcoq.mli | 2 +- parsing/egramml.ml | 2 +- parsing/egramml.mli | 2 +- parsing/g_constr.ml4 | 4 ++-- parsing/g_ltac.ml4 | 6 +++--- parsing/g_prim.ml4 | 2 +- parsing/g_proofs.ml4 | 2 +- parsing/g_tactic.ml4 | 32 +++++++++++++++++++++++++++----- parsing/g_vernac.ml4 | 2 +- parsing/lexer.ml4 | 8 +++++++- parsing/lexer.mli | 4 +++- parsing/pcoq.ml4 | 2 +- parsing/pcoq.mli | 2 +- parsing/tok.ml | 3 ++- parsing/tok.mli | 2 +- 17 files changed, 55 insertions(+), 24 deletions(-) (limited to 'parsing') diff --git a/parsing/compat.ml4 b/parsing/compat.ml4 index eba1d2b8..d1d55c81 100644 --- a/parsing/compat.ml4 +++ b/parsing/compat.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* CGeneralization (!@loc, Explicit, None, c) - | "$("; tac = Tactic.tactic; ")$" -> + | "ltac:"; "("; tac = Tactic.tactic_expr; ")" -> let arg = Genarg.in_gen (Genarg.rawwit Constrarg.wit_tactic) tac in CHole (!@loc, None, IntroAnonymous, Some arg) ] ] diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index a4dba506..959b0e89 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* arg_of_expr a - | IDENT "ltac"; ":"; n = natural -> TacGeneric (genarg_of_int n) + [ [ "ltac:"; a = tactic_expr LEVEL "0" -> arg_of_expr a + | "ltac:"; n = natural -> TacGeneric (genarg_of_int n) | a = tactic_top_or_arg -> a | r = reference -> Reference r | c = Constr.constr -> ConstrMayEval (ConstrTerm c) diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 84da9c42..5297c163 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* err ()) | _ -> err ()) +(* Hack to recognize "(x)" *) +let test_lpar_id_rpar = + Gram.Entry.of_parser "lpar_id_coloneq" + (fun strm -> + match get_tok (stream_nth 0 strm) with + | KEYWORD "(" -> + (match get_tok (stream_nth 1 strm) with + | IDENT _ -> + (match get_tok (stream_nth 2 strm) with + | KEYWORD ")" -> () + | _ -> err ()) + | _ -> err ()) + | _ -> err ()) + (* idem for (x:=t) and (1:=t) *) let test_lpar_idnum_coloneq = Gram.Entry.of_parser "test_lpar_idnum_coloneq" @@ -224,8 +238,9 @@ GEXTEND Gram ; induction_arg: [ [ n = natural -> (None,ElimOnAnonHyp n) + | test_lpar_id_rpar; c = constr_with_bindings -> + (Some false,induction_arg_of_constr c) | c = constr_with_bindings -> (None,induction_arg_of_constr c) - | "!"; c = constr_with_bindings -> (Some false,induction_arg_of_constr c) ] ] ; constr_with_bindings_arg: @@ -296,11 +311,18 @@ GEXTEND Gram | "**" -> !@loc, IntroForthcoming false ]] ; simple_intropattern: + [ [ pat = simple_intropattern_closed; + l = LIST0 ["%"; c = operconstr LEVEL "0" -> c] -> + let loc0,pat = pat in + let f c pat = + let loc = Loc.merge loc0 (Constrexpr_ops.constr_loc c) in + IntroAction (IntroApplyOn (c,(loc,pat))) in + !@loc, List.fold_right f l pat ] ] + ; + simple_intropattern_closed: [ [ pat = or_and_intropattern -> !@loc, IntroAction (IntroOrAndPattern pat) | pat = equality_intropattern -> !@loc, IntroAction pat | "_" -> !@loc, IntroAction IntroWildcard - | pat = simple_intropattern; "/"; c = constr -> - !@loc, IntroAction (IntroApplyOn (c,pat)) | pat = naming_intropattern -> !@loc, IntroNaming pat ] ] ; simple_binding: @@ -399,7 +421,7 @@ GEXTEND Gram | -> [] ] ] ; in_hyp_as: - [ [ "in"; id = id_or_meta; ipat = as_ipat -> Some (None,id,ipat) + [ [ "in"; id = id_or_meta; ipat = as_ipat -> Some (id,ipat) | -> None ] ] ; orient: diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 1f9f57f6..839f768b 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* ] -> string in_comments bp (store len c) s | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_string +(* Hook for exporting comment into xml theory files *) +let (f_xml_output_comment, xml_output_comment) = Hook.make ~default:ignore () + (* Utilities for comments in beautify *) let comment_begin = ref None let comm_loc bp = match !comment_begin with @@ -340,6 +343,9 @@ let null_comment s = let comment_stop ep = let current_s = Buffer.contents current in + if !Flags.xml_export && Buffer.length current > 0 && + (!between_com || not(null_comment current_s)) then + Hook.get f_xml_output_comment current_s; (if Flags.do_beautify() && Buffer.length current > 0 && (!between_com || not(null_comment current_s)) then let bp = match !comment_begin with diff --git a/parsing/lexer.mli b/parsing/lexer.mli index 2b9bd37d..24b0ec84 100644 --- a/parsing/lexer.mli +++ b/parsing/lexer.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* com_state val restore_com_state: com_state -> unit +val xml_output_comment : (string -> unit) Hook.t + val terminal : string -> Tok.t (** The lexer of Coq: *) diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 2e47e07a..32dbeaa4 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* CString.equal s1 s2 | KEYWORD s1, KEYWORD s2 -> CString.equal s1 s2 | METAIDENT s1, METAIDENT s2 -> CString.equal s1 s2 | PATTERNIDENT s1, PATTERNIDENT s2 -> CString.equal s1 s2 diff --git a/parsing/tok.mli b/parsing/tok.mli index feee1983..df006601 100644 --- a/parsing/tok.mli +++ b/parsing/tok.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*