Merge branch 'v8.5' into trunk

5 files changed, 8 insertions, 5 deletions

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/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/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 ->
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index cf6435fec4..54edbb2c88 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 dbd2aadf9d..2146ad964f 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