diff options
Diffstat (limited to 'parsing')
-rw-r--r-- | parsing/compat.ml4 | 2 | ||||
-rw-r--r-- | parsing/egramcoq.ml | 2 | ||||
-rw-r--r-- | parsing/egramcoq.mli | 2 | ||||
-rw-r--r-- | parsing/egramml.ml | 2 | ||||
-rw-r--r-- | parsing/egramml.mli | 2 | ||||
-rw-r--r-- | parsing/g_constr.ml4 | 4 | ||||
-rw-r--r-- | parsing/g_ltac.ml4 | 6 | ||||
-rw-r--r-- | parsing/g_prim.ml4 | 2 | ||||
-rw-r--r-- | parsing/g_proofs.ml4 | 2 | ||||
-rw-r--r-- | parsing/g_tactic.ml4 | 32 | ||||
-rw-r--r-- | parsing/g_vernac.ml4 | 2 | ||||
-rw-r--r-- | parsing/lexer.ml4 | 8 | ||||
-rw-r--r-- | parsing/lexer.mli | 4 | ||||
-rw-r--r-- | parsing/pcoq.ml4 | 2 | ||||
-rw-r--r-- | parsing/pcoq.mli | 2 | ||||
-rw-r--r-- | parsing/tok.ml | 3 | ||||
-rw-r--r-- | parsing/tok.mli | 2 |
17 files changed, 55 insertions, 24 deletions
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 *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 01194c60..b0bbdd81 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli index 2b0f7da8..964bd541 100644 --- a/parsing/egramcoq.mli +++ b/parsing/egramcoq.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/egramml.ml b/parsing/egramml.ml index 8fe03b36..3896970c 100644 --- a/parsing/egramml.ml +++ b/parsing/egramml.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/egramml.mli b/parsing/egramml.mli index 9ebb5b83..f71c368a 100644 --- a/parsing/egramml.mli +++ b/parsing/egramml.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index e2e6795f..5edb7b80 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -218,7 +218,7 @@ GEXTEND Gram CGeneralization (!@loc, Implicit, None, c) | "`("; c = operconstr LEVEL "200"; ")" -> 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 *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -134,8 +134,8 @@ GEXTEND Gram ; (* Tactic arguments *) tactic_arg: - [ [ IDENT "ltac"; ":"; a = tactic_expr LEVEL "0" -> 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 *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 017f0ea5..422384f3 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index c94ac846..2a00a176 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -44,6 +44,20 @@ let test_lpar_id_coloneq = | _ -> 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 *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index c6d5f3b9..5d96873f 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -298,6 +298,9 @@ let rec string in_comments bp len = parser | [< 'c; s >] -> 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 *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -29,6 +29,8 @@ type com_state val com_state: unit -> 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 *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 2146ad96..24b58775 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/tok.ml b/parsing/tok.ml index efd57968..c96b53de 100644 --- a/parsing/tok.ml +++ b/parsing/tok.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -21,6 +21,7 @@ type t = | EOI let equal t1 t2 = match t1, t2 with +| IDENT s1, KEYWORD s2 -> 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 *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |