From e8b4756c655eacd8a2b9b23630ba02dbbbc4e96e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 27 Mar 2015 18:17:03 +0100 Subject: Putting the From parameter of the Require command into the AST. --- parsing/g_vernac.ml4 | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'parsing') diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 70a8ec5522..cf7f6af28b 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 -> -- cgit v1.2.3 From b4f2e48b9e128a62d63668621844b571d3449cbf Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 30 Mar 2015 11:13:41 +0200 Subject: grammar: export hypident This is necessary to make ssr compile with both camlp4/5 --- parsing/g_tactic.ml4 | 2 +- parsing/pcoq.ml4 | 1 + parsing/pcoq.mli | 1 + 3 files changed, 3 insertions(+), 1 deletion(-) (limited to 'parsing') diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index b42b2c6dd3..69593f993c 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/pcoq.ml4 b/parsing/pcoq.ml4 index cf6435fec4..6a9848c1ca 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -375,6 +375,7 @@ 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 uconstr = make_gen_entry utactic (rawwit wit_uconstr) "uconstr" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index dbd2aadf9d..e23b65e12c 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -215,6 +215,7 @@ 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 uconstr : constr_expr Gram.entry val quantified_hypothesis : quantified_hypothesis Gram.entry -- cgit v1.2.3 From 41e4725805588b3fffdfdc0cd5ee6859de1612b5 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 30 Mar 2015 11:26:58 +0200 Subject: grammar: export constr_eval --- parsing/g_ltac.ml4 | 2 +- parsing/pcoq.ml4 | 1 + parsing/pcoq.mli | 1 + 3 files changed, 3 insertions(+), 1 deletion(-) (limited to 'parsing') diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 3cd7dbc9be..a4dba506d2 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 "|" -> diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 6a9848c1ca..54edbb2c88 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -377,6 +377,7 @@ module Tactic = 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 e23b65e12c..2146ad964f 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -217,6 +217,7 @@ module Tactic : 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