From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 parsing/g_proofs.ml4 | 66 +++++++++++++++++++++++++++++++++-------------------
 1 file changed, 42 insertions(+), 24 deletions(-)

(limited to 'parsing/g_proofs.ml4')

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
-- 
cgit v1.2.3