Merge branch 'master' into ltac2-hooks

13 files changed, 89 insertions, 59 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 7c5efaea3..1cb417bf4 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -397,33 +397,18 @@ let convert_to_hyp_tac c1 t1 c2 t2 p =
        simplest_elim false_t]
   end }
 
-let discriminate_tac (cstr,u as cstru) p =
+(* Essentially [assert (Heq : lhs = rhs) by proof_tac p; discriminate Heq] *)
+let discriminate_tac cstru p =
   Proofview.Goal.enter { enter = begin fun gl ->
-    let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
+    let lhs=constr_of_term p.p_lhs and rhs=constr_of_term p.p_rhs in
     let env = Proofview.Goal.env gl in
-    let concl = Proofview.Goal.concl gl in
-    let xid = Tacmach.New.pf_get_new_id (Id.of_string "X") gl in
-    let identity = Universes.constr_of_global (Lazy.force _I) in
-    let identity = EConstr.of_constr identity in
-    let trivial = Universes.constr_of_global (Lazy.force _True) in
-    let trivial = EConstr.of_constr trivial in
     let evm = Tacmach.New.project gl in
-    let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl t1) in
-    let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm in
-    let outtype = mkSort outtype in
-    let pred = mkLambda(Name xid,outtype,mkRel 1) in
+    let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl lhs) in
     let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in
-    let proj = build_projection intype cstru trivial concl gl in
-    let injt = app_global _f_equal
-			[|intype;outtype;proj;t1;t2;mkVar hid|] in
-    let endt k =
-      injt (fun injt ->
-            app_global _eq_rect
-		       [|outtype;trivial;pred;identity;concl;injt|] k) in
-    let neweq = app_global _eq [|intype;t1;t2|] in
+    let neweq=app_global _eq [|intype;lhs;rhs|] in
     Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm)
 			  (Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
-      [proof_tac p; endt refine_exact_check])
+      [proof_tac p; Equality.discrHyp hid])
   end }
 
 (* wrap everything *)
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 53b726432..ec3a49df4 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -274,6 +274,26 @@ ARGUMENT EXTEND in_clause
 | [ in_clause'(cl) ] -> [ cl ]
 END
 
+let local_test_lpar_id_colon =
+  let err () = raise Stream.Failure in
+  Pcoq.Gram.Entry.of_parser "lpar_id_colon"
+    (fun strm ->
+      match Util.stream_nth 0 strm with
+        | Tok.KEYWORD "(" ->
+            (match Util.stream_nth 1 strm with
+              | Tok.IDENT _ ->
+                  (match Util.stream_nth 2 strm with
+                    | Tok.KEYWORD ":" -> ()
+                    | _ -> err ())
+              | _ -> err ())
+        | _ -> err ())
+
+let pr_lpar_id_colon _ _ _ _ = mt ()
+
+ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY pr_lpar_id_colon
+| [ local_test_lpar_id_colon(x) ] -> [ () ]
+END
+
 (* spiwack: the print functions are incomplete, but I don't know what they are
 	used for *)
 let pr_r_nat_field natf =
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index 7d4bccfad..9b4167512 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -67,6 +67,10 @@ val pr_by_arg_tac :
   (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.std_ppcmds) ->
   raw_tactic_expr option -> Pp.std_ppcmds
 
+val test_lpar_id_colon : unit Pcoq.Gram.entry
+
+val wit_test_lpar_id_colon : (unit, unit, unit) Genarg.genarg_type
+
 (** Spiwack: Primitive for retroknowledge registration *)
 
 val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 21419d1f9..bd48614db 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -463,7 +463,7 @@ open Evar_tactics
 (* TODO: add support for some test similar to g_constr.name_colon so that
    expressions like "evar (list A)" do not raise a syntax error *)
 TACTIC EXTEND evar
-  [ "evar" "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ]
+  [ "evar" test_lpar_id_colon "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ]
 | [ "evar" constr(typ) ] -> [ let_evar Anonymous typ ]
 END
 
@@ -812,6 +812,19 @@ TACTIC EXTEND destauto
 | [ "destauto" "in" hyp(id) ] -> [ destauto_in id ]
 END
 
+(**********************************************************************)
+
+(**********************************************************************)
+(* A version of abstract constructing transparent terms               *)
+(* Introduced by Jason Gross and Benjamin Delaware in June 2016       *)
+(**********************************************************************)
+
+TACTIC EXTEND transparent_abstract
+| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.nf_enter { enter = fun gl ->
+      Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) } ]
+| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.nf_enter { enter = fun gl ->
+      Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) } ]
+END
 
 (* ********************************************************************* *)
 
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index ca5d198c2..d717ed0a5 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -460,7 +460,9 @@ END
 
 let pr_ltac_production_item = function
 | Tacentries.TacTerm s -> quote (str s)
-| Tacentries.TacNonTerm (_, (arg, sep), id) ->
+| Tacentries.TacNonTerm (_, (arg, None), None) -> str arg
+| Tacentries.TacNonTerm (_, (arg, Some _), None) -> assert false
+| Tacentries.TacNonTerm (_, (arg, sep), Some id) ->
   let sep = match sep with
   | None -> mt ()
   | Some sep -> str "," ++ spc () ++ quote (str sep)
@@ -470,7 +472,9 @@ let pr_ltac_production_item = function
 VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item
 | [ string(s) ] -> [ Tacentries.TacTerm s ]
 | [ ident(nt) "(" ident(p) ltac_production_sep_opt(sep) ")" ] ->
-  [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, sep), p) ]
+  [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, sep), Some p) ]
+| [ ident(nt) ] ->
+  [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, None), None) ]
 END
 
 VERNAC COMMAND EXTEND VernacTacticNotation
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 4b3ca80af..e33c25cf8 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -72,18 +72,7 @@ let test_lpar_idnum_coloneq =
         | _ -> err ())
 
 (* idem for (x:t) *)
-let test_lpar_id_colon =
-  Gram.Entry.of_parser "lpar_id_colon"
-    (fun strm ->
-      match stream_nth 0 strm with
-        | KEYWORD "(" ->
-            (match stream_nth 1 strm with
-              | IDENT _ ->
-                  (match stream_nth 2 strm with
-                    | KEYWORD ":" -> ()
-                    | _ -> err ())
-              | _ -> err ())
-        | _ -> err ())
+open Extraargs
 
 (* idem for (x1..xn:t) [n^2 complexity but exceptional use] *)
 let check_for_coloneq =
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index b73b66e56..a61957559 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -51,7 +51,7 @@ let pr_global x = Nametab.pr_global_env Id.Set.empty x
 
 type 'a grammar_tactic_prod_item_expr =
 | TacTerm of string
-| TacNonTerm of Loc.t * 'a * Names.Id.t
+| TacNonTerm of Loc.t * 'a * Names.Id.t option
 
 type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list
 
@@ -264,8 +264,9 @@ type 'a extra_genarg_printer =
       let rec pack prods args = match prods, args with
       | [], [] -> []
       | TacTerm s :: prods, args -> TacTerm s :: pack prods args
-      | TacNonTerm (loc, symb, id) :: prods, arg :: args ->
-        TacNonTerm (loc, (symb, arg), id) :: pack prods args
+      | TacNonTerm (_, _, None) :: prods, args -> pack prods args
+      | TacNonTerm (loc, symb, (Some _ as ido)) :: prods, arg :: args ->
+        TacNonTerm (loc, (symb, arg), ido) :: pack prods args
       | _ -> raise Not_found
       in
       let prods = pack pp.pptac_prods l in
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 729338fb9..433f342c4 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -21,7 +21,7 @@ open Ppextend
 
 type 'a grammar_tactic_prod_item_expr =
 | TacTerm of string
-| TacNonTerm of Loc.t * 'a * Names.Id.t
+| TacNonTerm of Loc.t * 'a * Names.Id.t option
 
 type 'a raw_extra_genarg_printer =
     (constr_expr -> std_ppcmds) ->
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 32750383b..91262f6fd 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -21,7 +21,7 @@ open Nameops
 
 type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr =
 | TacTerm of string
-| TacNonTerm of Loc.t * 'a * Names.Id.t
+| TacNonTerm of Loc.t * 'a * Names.Id.t option
 
 type raw_argument = string * string option
 type argument = Genarg.ArgT.any Extend.user_symbol
@@ -174,9 +174,9 @@ let add_tactic_entry (kn, ml, tg) state =
   in
   let map = function
   | TacTerm s -> GramTerminal s
-  | TacNonTerm (loc, s, _) ->
+  | TacNonTerm (loc, s, ido) ->
     let EntryName (typ, e) = prod_item_of_symbol tg.tacgram_level s in
-    GramNonTerminal (loc, typ, e)
+    GramNonTerminal (loc, Option.map (fun _ -> typ) ido, e)
   in
   let prods = List.map map tg.tacgram_prods in
   let rules = make_rule mkact prods in
@@ -202,7 +202,7 @@ let register_tactic_notation_entry name entry =
 
 let interp_prod_item = function
   | TacTerm s -> TacTerm s
-  | TacNonTerm (loc, (nt, sep), id) ->
+  | TacNonTerm (loc, (nt, sep), ido) ->
     let symbol = parse_user_entry nt sep in
     let interp s = function
     | None ->
@@ -220,7 +220,7 @@ let interp_prod_item = function
       end
     in
     let symbol = interp_entry_name interp symbol in
-    TacNonTerm (loc, symbol, id)
+    TacNonTerm (loc, symbol, ido)
 
 let make_fresh_key =
   let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in
@@ -296,7 +296,7 @@ let inTacticGrammar : tactic_grammar_obj -> obj =
 
 let cons_production_parameter = function
 | TacTerm _ -> None
-| TacNonTerm (_, _, id) -> Some id
+| TacNonTerm (_, _, ido) -> ido
 
 let add_glob_tactic_notation local ~level prods forml ids tac =
   let parule = {
@@ -362,7 +362,7 @@ let add_ml_tactic_notation name ~level prods =
     let open Tacexpr in
     let get_id = function
     | TacTerm s -> None
-    | TacNonTerm (_, _, id) -> Some id
+    | TacNonTerm (_, _, ido) -> ido
     in
     let ids = List.map_filter get_id prods in
     let entry = { mltac_name = name; mltac_index = len - i - 1 } in
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 069504473..dac62dad3 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -20,7 +20,7 @@ val register_ltac : locality_flag -> Tacexpr.tacdef_body list -> unit
 
 type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr =
 | TacTerm of string
-| TacNonTerm of Loc.t * 'a * Names.Id.t
+| TacNonTerm of Loc.t * 'a * Names.Id.t option
 
 type raw_argument = string * string option
 (** An argument type as provided in Tactic notations, i.e. a string like
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index dffeade29..dac15ff79 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -85,6 +85,19 @@ let skipped = Proofview.NonLogical.run (Proofview.NonLogical.ref 0)
 let skip = Proofview.NonLogical.run (Proofview.NonLogical.ref 0)
 let breakpoint = Proofview.NonLogical.run (Proofview.NonLogical.ref None)
 
+let batch = ref false
+
+open Goptions
+
+let _ =
+  declare_bool_option
+    { optsync  = false;
+      optdepr  = false;
+      optname  = "Ltac batch debug";
+      optkey   = ["Ltac";"Batch";"Debug"];
+      optread  = (fun () -> !batch);
+      optwrite = (fun x -> batch := x) }
+
 let rec drop_spaces inst i =
   if String.length inst > i && inst.[i] == ' ' then drop_spaces inst (i+1)
   else i
@@ -150,6 +163,7 @@ let rec prompt level =
   begin
     let open Proofview.NonLogical in
     Proofview.NonLogical.print_notice (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >>
+    if Pervasives.(!batch) then return (DebugOn (level+1)) else
     let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in
     Proofview.NonLogical.catch Proofview.NonLogical.read_line
       begin function (e, info) -> match e with
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index fc9d70ae7..c649cfb2c 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -8,7 +8,7 @@
 
 (* The `Quote' tactic *)
 
-(* The basic idea is to automatize the inversion of interpetation functions
+(* The basic idea is to automatize the inversion of interpretation functions
    in 2-level approach
 
    Examples are given in \texttt{theories/DEMOS/DemoQuote.v}
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index d59ffee54..6b8ef630a 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -333,12 +333,12 @@ let _ = add_map "ring"
     my_reference "gen_phiZ", (function _->Eval);
     (* Pphi_dev: evaluate polynomial and coef operations, protect
        ring operations and make recursive call on the var map *)
-    pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot);
+    pol_cst "Pphi_dev", (function -1|8|9|10|12|14->Eval|11|13->Rec|_->Prot);
     pol_cst "Pphi_pow",
           (function -1|8|9|10|13|15|17->Eval|11|16->Rec|_->Prot);
-    (* PEeval: evaluate morphism and polynomial, protect ring
+    (* PEeval: evaluate polynomial, protect ring
        operations and make recursive call on the var map *)
-    pol_cst "PEeval", (function -1|8|10|13->Eval|12->Rec|_->Prot)])
+    pol_cst "PEeval", (function -1|10|13->Eval|8|12->Rec|_->Prot)])
 
 (****************************************************************************)
 (* Ring database *)
@@ -780,20 +780,20 @@ let _ = add_map "field"
     (* display_linear: evaluate polynomials and coef operations, protect
        field operations and make recursive call on the var map *)
     my_reference "display_linear",
-      (function -1|9|10|11|12|13|15|16->Eval|14->Rec|_->Prot);
+      (function -1|9|10|11|13|15|16->Eval|12|14->Rec|_->Prot);
     my_reference "display_pow_linear",
      (function -1|9|10|11|14|16|18|19->Eval|12|17->Rec|_->Prot);
    (* Pphi_dev: evaluate polynomial and coef operations, protect
        ring operations and make recursive call on the var map *)
-    pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot);
+    pol_cst "Pphi_dev", (function -1|8|9|10|12|14->Eval|11|13->Rec|_->Prot);
     pol_cst "Pphi_pow",
-          (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot);
-    (* PEeval: evaluate morphism and polynomial, protect ring
+          (function -1|8|9|10|13|15|17->Eval|11|16->Rec|_->Prot);
+    (* PEeval: evaluate polynomial, protect ring
        operations and make recursive call on the var map *)
-    pol_cst "PEeval", (function -1|8|10|13->Eval|12->Rec|_->Prot);
-    (* FEeval: evaluate morphism, protect field
+    pol_cst "PEeval", (function -1|10|13->Eval|8|12->Rec|_->Prot);
+    (* FEeval: evaluate polynomial, protect field
        operations and make recursive call on the var map *)
-    my_reference "FEeval", (function -1|10|12|15->Eval|14->Rec|_->Prot)]);;
+    my_reference "FEeval", (function -1|12|15->Eval|10|14->Rec|_->Prot)]);;
 
 let _ = add_map "field_cond"
   (map_without_eq