diff options
Diffstat (limited to 'parsing/g_proofs.ml4')
| -rw-r--r-- | parsing/g_proofs.ml4 | 66 |
1 files changed, 42 insertions, 24 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 557972ce..27f14c79 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -1,24 +1,31 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pcoq -open Pp -open Tactic -open Util -open Vernac_ -open Topconstr +open Compat +open Constrexpr open Vernacexpr -open Prim -open Constr +open Misctypes open Tok +open Pcoq +open Pcoq.Tactic +open Pcoq.Prim +open Pcoq.Constr +open Pcoq.Vernac_ + let thm_token = G_vernac.thm_token +let hint_proof_using e = function + | Some _ as x -> x + | None -> match Proof_using.get_default_proof_using () with + | None -> None + | Some s -> Some (Gram.entry_parse e (Gram.parsable (Stream.of_string s))) + (* Proof commands *) GEXTEND Gram GLOBAL: command; @@ -29,12 +36,13 @@ GEXTEND Gram ; command: [ [ IDENT "Goal"; c = lconstr -> VernacGoal c - | IDENT "Proof" -> VernacProof (None,None) + | IDENT "Proof" -> + VernacProof (None,hint_proof_using G_vernac.section_subset_descr None) | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn | IDENT "Proof"; "with"; ta = tactic; - l = OPT [ "using"; l = LIST0 identref -> l ] -> - VernacProof (Some ta, l) - | IDENT "Proof"; "using"; l = LIST0 identref; + l = OPT [ "using"; l = G_vernac.section_subset_descr -> l ] -> + VernacProof (Some ta,hint_proof_using G_vernac.section_subset_descr l) + | IDENT "Proof"; "using"; l = G_vernac.section_subset_descr; ta = OPT [ "with"; ta = tactic -> ta ] -> VernacProof (ta,Some l) | IDENT "Proof"; c = lconstr -> VernacExactProof c @@ -70,6 +78,7 @@ GEXTEND Gram | IDENT "Show"; IDENT "Node" -> VernacShow ShowNode | IDENT "Show"; IDENT "Script" -> VernacShow ShowScript | IDENT "Show"; IDENT "Existentials" -> VernacShow ShowExistentials + | IDENT "Show"; IDENT "Universes" -> VernacShow ShowUniverses | IDENT "Show"; IDENT "Tree" -> VernacShow ShowTree | IDENT "Show"; IDENT "Conjectures" -> VernacShow ShowProofNames | IDENT "Show"; IDENT "Proof" -> VernacShow ShowProof @@ -81,29 +90,35 @@ GEXTEND Gram (* Hints for Auto and EAuto *) | IDENT "Create"; IDENT "HintDb" ; id = IDENT ; b = [ "discriminated" -> true | -> false ] -> - VernacCreateHintDb (use_module_locality (), id, b) + VernacCreateHintDb (id, b) | IDENT "Remove"; IDENT "Hints"; ids = LIST1 global; dbnames = opt_hintbases -> - VernacRemoveHints (use_module_locality (), dbnames, ids) + VernacRemoveHints (dbnames, ids) | IDENT "Hint"; local = obsolete_locality; h = hint; dbnames = opt_hintbases -> - VernacHints (enforce_module_locality local,dbnames, h) + VernacHints (local,dbnames, h) (* Declare "Resolve" explicitly so as to be able to later extend with "Resolve ->" and "Resolve <-" *) - | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 constr; n = OPT natural; + | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference_or_constr; + pri = OPT [ "|"; i = natural -> i ]; dbnames = opt_hintbases -> - VernacHints (use_module_locality (),dbnames, - HintsResolve (List.map (fun x -> (n, true, x)) lc)) + VernacHints (false,dbnames, + HintsResolve (List.map (fun x -> (pri, true, x)) lc)) ] ]; - obsolete_locality: [ [ IDENT "Local" -> true | -> false ] ] ; + reference_or_constr: + [ [ r = global -> HintsReference r + | c = constr -> HintsConstr c ] ] + ; hint: - [ [ IDENT "Resolve"; lc = LIST1 constr; n = OPT natural -> - HintsResolve (List.map (fun x -> (n, true, x)) lc) - | IDENT "Immediate"; lc = LIST1 constr -> HintsImmediate lc + [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; + pri = OPT [ "|"; i = natural -> i ] -> + HintsResolve (List.map (fun x -> (pri, true, x)) lc) + | IDENT "Immediate"; lc = LIST1 reference_or_constr -> HintsImmediate lc | IDENT "Transparent"; lc = LIST1 global -> HintsTransparency (lc, true) | IDENT "Opaque"; lc = LIST1 global -> HintsTransparency (lc, false) + | IDENT "Mode"; l = global; m = mode -> HintsMode (l, m) | IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc | IDENT "Extern"; n = natural; c = OPT constr_pattern ; "=>"; @@ -112,6 +127,9 @@ GEXTEND Gram ; constr_body: [ [ ":="; c = lconstr -> c - | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c, Glob_term.CastConv (Term.DEFAULTcast,t)) ] ] + | ":"; t = lconstr; ":="; c = lconstr -> CCast(!@loc,c,CastConv t) ] ] + ; + mode: + [ [ l = LIST1 ["+" -> true | "-" -> false] -> l ] ] ; END |