Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg

7 files changed, 22 insertions, 13 deletions

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