From 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 15 Jul 2015 10:36:12 +0200 Subject: Imported Upstream version 8.5~beta2+dfsg --- parsing/g_constr.ml4 | 2 +- parsing/g_ltac.ml4 | 8 ++++++-- parsing/g_proofs.ml4 | 14 ++++++++------ parsing/g_tactic.ml4 | 2 +- parsing/g_vernac.ml4 | 5 ++--- parsing/pcoq.ml4 | 2 ++ parsing/pcoq.mli | 2 ++ 7 files changed, 22 insertions(+), 13 deletions(-) (limited to 'parsing') diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 8246df28..3bb029a8 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -157,7 +157,7 @@ GEXTEND Gram ] ] ; universe: - [ [ "max("; ids = LIST1 ident SEP ","; ")" -> ids + [ [ IDENT "max"; "("; ids = LIST1 ident SEP ","; ")" -> ids | id = ident -> [id] ] ] ; diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index b4d96e5c..a4dba506 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -33,7 +33,7 @@ let genarg_of_ipattern pat = in_gen (rawwit Constrarg.wit_intro_pattern) pat GEXTEND Gram GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg - constr_may_eval; + constr_may_eval constr_eval; tactic_then_last: [ [ "|"; lta = LIST0 OPT tactic_expr SEP "|" -> @@ -153,8 +153,12 @@ GEXTEND Gram | IDENT "type_term"; c=uconstr -> TacPretype c | IDENT "numgoals" -> TacNumgoals ] ] ; + (* If a qualid is given, use its short name. TODO: have the shortest + non ambiguous name where dots are replaced by "_"? Probably too + verbose most of the time. *) fresh_id: - [ [ s = STRING -> ArgArg s | id = ident -> ArgVar (!@loc,id) ] ] + [ [ s = STRING -> ArgArg s (*| id = ident -> ArgVar (!@loc,id)*) + | qid = qualid -> let (_pth,id) = Libnames.repr_qualid (snd qid) in ArgVar (!@loc,id) ] ] ; constr_eval: [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 27f14c79..1e254c16 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -52,15 +52,17 @@ GEXTEND Gram | IDENT "Existential"; n = natural; c = constr_body -> VernacSolveExistential (n,c) | IDENT "Admitted" -> VernacEndProof Admitted - | IDENT "Qed" -> VernacEndProof (Proved (true,None)) - | IDENT "Save" -> VernacEndProof (Proved (true,None)) + | IDENT "Qed" -> VernacEndProof (Proved (Opaque None,None)) + | IDENT "Qed"; IDENT "exporting"; l = LIST0 identref SEP "," -> + VernacEndProof (Proved (Opaque (Some l),None)) + | IDENT "Save" -> VernacEndProof (Proved (Opaque None,None)) | IDENT "Save"; tok = thm_token; id = identref -> - VernacEndProof (Proved (true,Some (id,Some tok))) + VernacEndProof (Proved (Opaque None,Some (id,Some tok))) | IDENT "Save"; id = identref -> - VernacEndProof (Proved (true,Some (id,None))) - | IDENT "Defined" -> VernacEndProof (Proved (false,None)) + VernacEndProof (Proved (Opaque None,Some (id,None))) + | IDENT "Defined" -> VernacEndProof (Proved (Transparent,None)) | IDENT "Defined"; id=identref -> - VernacEndProof (Proved (false,Some (id,None))) + VernacEndProof (Proved (Transparent,Some (id,None))) | IDENT "Restart" -> VernacRestart | IDENT "Undo" -> VernacUndo 1 | IDENT "Undo"; n = natural -> VernacUndo n diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index b42b2c6d..69593f99 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -202,7 +202,7 @@ let merge_occurrences loc cl = function GEXTEND Gram GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis bindings red_expr int_or_var open_constr uconstr - simple_intropattern clause_dft_concl; + simple_intropattern clause_dft_concl hypident; int_or_var: [ [ n = integer -> ArgArg n diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 70a8ec55..cf7f6af2 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -465,11 +465,10 @@ GEXTEND Gram (* Requiring an already compiled module *) | IDENT "Require"; export = export_token; qidl = LIST1 global -> - VernacRequire (export, qidl) + VernacRequire (None, export, qidl) | IDENT "From" ; ns = global ; IDENT "Require"; export = export_token ; qidl = LIST1 global -> - let qidl = List.map (Libnames.join_reference ns) qidl in - VernacRequire (export, qidl) + VernacRequire (Some ns, export, qidl) | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl) | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl) | IDENT "Include"; e = module_type_inl; l = LIST0 ext_module_expr -> diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index cf6435fe..54edbb2c 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -375,7 +375,9 @@ module Tactic = make_gen_entry utactic (rawwit wit_constr_with_bindings) "constr_with_bindings" let bindings = make_gen_entry utactic (rawwit wit_bindings) "bindings" + let hypident = Gram.entry_create "hypident" let constr_may_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_may_eval" + let constr_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_may_eval" let uconstr = make_gen_entry utactic (rawwit wit_uconstr) "uconstr" let quantified_hypothesis = diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index dbd2aadf..2146ad96 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -215,7 +215,9 @@ module Tactic : val open_constr : open_constr_expr Gram.entry val constr_with_bindings : constr_expr with_bindings Gram.entry val bindings : constr_expr bindings Gram.entry + val hypident : (Id.t located * Locus.hyp_location_flag) Gram.entry val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry + val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry val uconstr : constr_expr Gram.entry val quantified_hypothesis : quantified_hypothesis Gram.entry val int_or_var : int or_var Gram.entry -- cgit v1.2.3