Closing bug #3260

adding a new grammar entry for clauses

15 files changed, 74 insertions, 126 deletions

diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 37e627a6d..c25e02c02 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -55,6 +55,9 @@ let wit_bindings = unsafe_of_type BindingsArgType
 
 let wit_red_expr = unsafe_of_type RedExprArgType
 
+let wit_clause_dft_concl  =
+  Genarg.make0 None "clause_dft_concl"
+
 (** Register location *)
 
 let () =
@@ -62,3 +65,4 @@ let () =
   register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern";
   register_name0 wit_tactic "Constrarg.wit_tactic";
   register_name0 wit_sort "Constrarg.wit_sort";
+  register_name0 wit_clause_dft_concl "Constrarg.wit_clause_dft_concl";
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index 5faef378a..d5d19f2ea 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -30,6 +30,7 @@ val wit_int_or_var : int or_var uniform_genarg_type
 
 val wit_intro_pattern : intro_pattern_expr located uniform_genarg_type
 
+
 val wit_ident : Id.t uniform_genarg_type
 
 val wit_var : (Id.t located, Id.t located, Id.t) genarg_type
@@ -68,3 +69,5 @@ val wit_red_expr :
   (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
 
 val wit_tactic : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type
+
+val wit_clause_dft_concl :  (Names.Id.t Loc.located Tacexpr.or_metaid Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 93afb3d5a..6b989b6ba 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -216,7 +216,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
-  simple_intropattern;
+  simple_intropattern clause_dft_concl;
 
   int_or_var:
     [ [ n = integer  -> ArgArg n
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 6fac3da96..473e095dc 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -388,6 +388,9 @@ module Tactic =
     let red_expr = make_gen_entry utactic (rawwit wit_red_expr) "red_expr"
     let simple_intropattern =
       make_gen_entry utactic (rawwit wit_intro_pattern) "simple_intropattern"
+    let clause_dft_concl = 
+      make_gen_entry utactic (rawwit wit_clause_dft_concl) "clause"
+
 
     (* Main entries for ltac *)
     let tactic_arg = Gram.entry_create "tactic:tactic_arg"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 3fb647a96..cf98e5a54 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -218,6 +218,7 @@ module Tactic :
     val red_expr : raw_red_expr Gram.entry
     val simple_tactic : raw_atomic_tactic_expr Gram.entry
     val simple_intropattern : intro_pattern_expr located Gram.entry
+    val clause_dft_concl : Names.Id.t Loc.located Tacexpr.or_metaid Locus.clause_expr Gram.entry
     val tactic_arg : raw_tactic_arg Gram.entry
     val tactic_expr : raw_tactic_expr Gram.entry
     val binder_tactic : raw_tactic_expr Gram.entry
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 520eac8ab..e74dd9fc1 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1034,6 +1034,12 @@ let () =
     Miscprint.pr_intro_pattern
     Miscprint.pr_intro_pattern
     Miscprint.pr_intro_pattern;
+  Genprint.register_print0
+    Constrarg.wit_clause_dft_concl
+    (pr_clauses (Some true) (pr_or_metaid pr_lident))
+    (pr_clauses (Some true) pr_lident)
+    (pr_clauses (Some true) (fun id -> pr_lident (Loc.ghost,id)))
+  ;
   Genprint.register_print0 Constrarg.wit_sort
     pr_glob_sort pr_glob_sort pr_sort;
   Genprint.register_print0 Stdarg.wit_int int int int;
diff --git a/printing/pptactic.mli b/printing/pptactic.mli
index e20e3ae01..7dbdf80aa 100644
--- a/printing/pptactic.mli
+++ b/printing/pptactic.mli
@@ -55,6 +55,8 @@ type pp_tactic = {
 val declare_ml_tactic_pprule : string -> pp_tactic -> unit
 val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
 
+val pr_clauses :  bool option ->
+           ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
 val pr_raw_generic :
   (constr_expr -> std_ppcmds) ->
   (constr_expr -> std_ppcmds) ->
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 65f030742..6c3c55efd 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -487,12 +487,12 @@ let autounfold_tac db cls gl =
   | Some [] -> ["core"]
   | Some l -> l
   in
-  autounfold dbs (Extraargs.glob_in_arg_hyp_to_clause cls) gl
+  autounfold dbs  cls gl
 
 open Extraargs
 
 TACTIC EXTEND autounfold
-| [ "autounfold" hintbases(db) in_arg_hyp(id) ] -> [ Proofview.V82.tactic (autounfold_tac db id) ]
+| [ "autounfold" hintbases(db) clause(cl) ] -> [ Proofview.V82.tactic (autounfold_tac db cl) ]
 END
 
 let unfold_head env (ids, csts) c = 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index f2062076c..a480f6de6 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -505,6 +505,24 @@ let rewriteRL = general_rewrite false AllOccurrences true true
 
 (* Replacing tactics *)
 
+let classes_dirpath =
+  DirPath.make (List.map Id.of_string ["Classes";"Coq"])
+
+let init_setoid () =
+  if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then ()
+  else Coqlib.check_required_library ["Coq";"Setoids";"Setoid"]
+
+let check_setoid cl = 
+  Option.fold_left
+    ( List.fold_left 
+	(fun b ((occ,_),_) -> 
+	  b||(Locusops.occurrences_map (fun x -> x) occ <> AllOccurrences)
+	)
+    )
+    ((Locusops.occurrences_map (fun x -> x) cl.concl_occs <> AllOccurrences) &&
+	(Locusops.occurrences_map (fun x -> x) cl.concl_occs <> NoOccurrences))
+    cl.onhyps
+    
 (* eq,sym_eq : equality on Type and its symmetry theorem
    c2 c1 : c1 is to be replaced by c2
    unsafe : If true, do not check that c1 and c2 are convertible
@@ -526,6 +544,8 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt =
     let e = build_coq_eq () in
     let sym = build_coq_eq_sym () in
     let eq = applist (e, [t1;c1;c2]) in
+    if check_setoid clause
+    then init_setoid ();
     tclTHENS (assert_as false None eq)
       [onLastHypId (fun id ->
 	tclTHEN
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index c156e869d..dc41cf8e3 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -208,94 +208,6 @@ END
 
 let pr_by_arg_tac prtac opt_c = pr_by_arg_tac () () prtac opt_c
 
-let pr_in_hyp  pr_id (lo,concl) :  Pp.std_ppcmds =
-  match lo,concl with
-    | Some [],true -> mt ()
-    | None,true -> str "in" ++ spc () ++ str "*"
-    | None,false -> str "in" ++ spc () ++ str "*" ++ spc () ++ str "|-"
-    | Some l,_ ->
-	str "in" ++
-         spc () ++ prlist_with_sep pr_comma pr_id l ++
-	  match concl with
-	    | true -> spc () ++ str "|-" ++ spc () ++ str "*"
-	    | _ -> mt ()
-
-
-let pr_in_arg_hyp _ _ _ = pr_in_hyp (fun (_,id) -> Ppconstr.pr_id id)
-
-let pr_in_arg_hyp_typed  _ _  _  = pr_in_hyp Ppconstr.pr_id
-
-
-let pr_var_list_gen pr_id = Pp.prlist_with_sep (fun () -> str ",") pr_id
-
-let pr_var_list_typed _ _ _ =  pr_var_list_gen Ppconstr.pr_id
-
-let pr_var_list _ _ _ = pr_var_list_gen (fun (_,id) -> Ppconstr.pr_id id)
-
-
-ARGUMENT EXTEND comma_var_lne
-  PRINTED BY pr_var_list_typed
-  RAW_TYPED AS var list
-  RAW_PRINTED BY pr_var_list
-  GLOB_TYPED AS var list
-  GLOB_PRINTED BY pr_var_list
-| [ var(x) ] -> [ [x] ]
-| [ var(x) "," comma_var_lne(l) ] -> [x::l]
-END
-
-ARGUMENT EXTEND comma_var_l
-  PRINTED BY pr_var_list_typed
-  RAW_TYPED AS var list
-  RAW_PRINTED BY pr_var_list
-  GLOB_TYPED AS var list
-  GLOB_PRINTED BY pr_var_list
-| [  comma_var_lne(l) ] -> [l]
-| [] -> [ [] ]
-END
-
-let pr_in_concl _ _ _ = function true -> str "|- " ++ spc () ++ str "*" | _ -> str "|-"
-
-ARGUMENT EXTEND inconcl
-  TYPED AS bool
-  PRINTED BY pr_in_concl
-| [ "|-" "*" ] -> [ true ]
-| [ "|-" ] -> [ false ]
-END
-
-
-
-ARGUMENT EXTEND in_arg_hyp
-  PRINTED BY pr_in_arg_hyp_typed
-  RAW_TYPED AS var list option * bool
-  RAW_PRINTED BY pr_in_arg_hyp
-  GLOB_TYPED AS var list option * bool
-  GLOB_PRINTED BY pr_in_arg_hyp
-| [ "in" "*" ] -> [(None,true)]
-| [ "in" "*" inconcl_opt(b) ] -> [let onconcl = match b with Some b -> b | None -> true in (None,onconcl)]
-| [ "in" comma_var_l(l) inconcl_opt(b) ] -> [ let onconcl = match b with Some b -> b | None -> false in
-					      Some l, onconcl
-					   ]
-| [ ] -> [ (Some [],true) ]
-END
-
-let pr_in_arg_hyp = pr_in_arg_hyp_typed () () ()
-
-let gen_in_arg_hyp_to_clause trad_id (hyps ,concl) : clause =
-  {onhyps=
-   Option.map
-     (fun l ->
-	List.map
-	  (fun id -> ( (AllOccurrences,trad_id id),InHyp))
-	  l
-     )
-     hyps;
-   concl_occs = if concl then AllOccurrences else NoOccurrences}
-
-
-let raw_in_arg_hyp_to_clause = gen_in_arg_hyp_to_clause snd
-let glob_in_arg_hyp_to_clause = gen_in_arg_hyp_to_clause (fun x -> x)
-
-
 (* spiwack argument for the commands of the retroknowledge *)
 
 let wit_r_nat_field =
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index 16c236b82..89ce61b2b 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -43,17 +43,6 @@ val wit_hloc : (loc_place, loc_place, place) Genarg.genarg_type
 val hloc : loc_place Pcoq.Gram.entry
 val pr_hloc : loc_place -> Pp.std_ppcmds
 
-val in_arg_hyp:  (Names.Id.t Loc.located list option * bool)  Pcoq.Gram.entry
-
-val wit_in_arg_hyp :
-  ((Names.Id.t Loc.located list option * bool),
-  (Names.Id.t Loc.located list option * bool),
-  (Names.Id.t list option * bool)) Genarg.genarg_type
-
-val raw_in_arg_hyp_to_clause : (Names.Id.t Loc.located list option * bool) -> Locus.clause
-val glob_in_arg_hyp_to_clause :  (Names.Id.t list option * bool)  -> Locus.clause
-val pr_in_arg_hyp : (Names.Id.t list option * bool) -> Pp.std_ppcmds
-
 val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.entry
 val wit_by_arg_tac :
   (raw_tactic_expr option,
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 28f8c2f40..1fbe5c482 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -30,36 +30,36 @@ TACTIC EXTEND admit
   [ "admit" ] -> [ admit_as_an_axiom ]
 END
 
-let replace_in_clause_maybe_by (sigma1,c1) c2 in_hyp tac =
+let replace_in_clause_maybe_by (sigma1,c1) c2 cl  tac =
   Tacticals.New.tclWITHHOLES false
-    (replace_in_clause_maybe_by c1 c2 (glob_in_arg_hyp_to_clause in_hyp))
+    (replace_in_clause_maybe_by c1 c2 cl)
     sigma1
     (Option.map Tacinterp.eval_tactic tac)
 
-let replace_multi_term dir_opt (sigma,c) in_hyp =
+let replace_multi_term dir_opt (sigma,c) cl =
   Tacticals.New.tclWITHHOLES false
     (replace_multi_term dir_opt c)
     sigma
-    (glob_in_arg_hyp_to_clause in_hyp)
+    cl
 
 TACTIC EXTEND replace
-   ["replace" open_constr(c1) "with" constr(c2) in_arg_hyp(in_hyp) by_arg_tac(tac) ]
--> [ replace_in_clause_maybe_by c1 c2 in_hyp tac ]
+   ["replace" open_constr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ]
+-> [ replace_in_clause_maybe_by c1 c2 cl tac ]
 END
 
 TACTIC EXTEND replace_term_left
-  [ "replace"  "->" open_constr(c) in_arg_hyp(in_hyp) ]
-  -> [ replace_multi_term (Some true) c in_hyp ]
+  [ "replace"  "->" open_constr(c) clause(cl) ]
+  -> [ replace_multi_term (Some true) c cl ]
 END
 
 TACTIC EXTEND replace_term_right
-  [ "replace"  "<-" open_constr(c) in_arg_hyp(in_hyp) ]
-  -> [ replace_multi_term (Some false) c in_hyp ]
+  [ "replace"  "<-" open_constr(c) clause(cl) ]
+  -> [ replace_multi_term (Some false) c cl ]
 END
 
 TACTIC EXTEND replace_term
-  [ "replace" open_constr(c) in_arg_hyp(in_hyp) ]
-  -> [ replace_multi_term None c in_hyp ]
+  [ "replace" open_constr(c) clause(cl) ]
+  -> [ replace_multi_term None c cl ]
 END
 
 let induction_arg_of_quantified_hyp = function
@@ -211,22 +211,19 @@ ARGUMENT EXTEND orient_string TYPED AS (bool * string) PRINTED BY pr_orient_stri
 END
 
 TACTIC EXTEND autorewrite
-| [ "autorewrite" "with" ne_preident_list(l) in_arg_hyp(cl) ] ->
-    [ auto_multi_rewrite  l (glob_in_arg_hyp_to_clause  cl) ]
-| [ "autorewrite" "with" ne_preident_list(l) in_arg_hyp(cl) "using" tactic(t) ] ->
+| [ "autorewrite" "with" ne_preident_list(l) clause(cl) ] ->
+    [ auto_multi_rewrite  l ( cl) ]
+| [ "autorewrite" "with" ne_preident_list(l) clause(cl) "using" tactic(t) ] ->
     [
-      let cl =  glob_in_arg_hyp_to_clause cl in
       auto_multi_rewrite_with (Tacinterp.eval_tactic t) l cl
-
     ]
 END
 
 TACTIC EXTEND autorewrite_star
-| [ "autorewrite" "*" "with" ne_preident_list(l) in_arg_hyp(cl) ] ->
-    [ auto_multi_rewrite ~conds:AllMatches l (glob_in_arg_hyp_to_clause  cl) ]
-| [ "autorewrite" "*" "with" ne_preident_list(l) in_arg_hyp(cl) "using" tactic(t) ] ->
-    [ let cl =  glob_in_arg_hyp_to_clause cl in
-	auto_multi_rewrite_with ~conds:AllMatches (Tacinterp.eval_tactic t) l cl ]
+| [ "autorewrite" "*" "with" ne_preident_list(l) clause(cl) ] ->
+    [ auto_multi_rewrite ~conds:AllMatches l cl ]
+| [ "autorewrite" "*" "with" ne_preident_list(l) clause(cl) "using" tactic(t) ] ->
+  [ auto_multi_rewrite_with ~conds:AllMatches (Tacinterp.eval_tactic t) l cl ]
 END
 
 (**********************************************************************)
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 9b50cc1c0..cd2319c01 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -793,6 +793,13 @@ let () =
   Genintern.register_intern0 wit_intro_pattern intern_intro_pattern
 
 let () =
+  let intern_clause ist cl =
+    let ans = clause_app (intern_hyp_location ist) cl in
+    (ist, ans)
+  in
+  Genintern.register_intern0 wit_clause_dft_concl intern_clause
+
+let () =
   Genintern.register_intern0 wit_ref (lift intern_global_reference);
   Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg);
   Genintern.register_intern0 wit_sort (fun ist s -> (ist, s))
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 3d9091189..8c4cec0c2 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -393,7 +393,7 @@ let interp_occurrences ist occs =
 let interp_hyp_location ist gl ((occs,id),hl) =
   ((interp_occurrences ist occs,interp_hyp ist gl id),hl)
 
-let interp_clause ist gl { onhyps=ol; concl_occs=occs } =
+let interp_clause ist gl { onhyps=ol; concl_occs=occs } : clause =
   { onhyps=Option.map(List.map (interp_hyp_location ist gl)) ol;
     concl_occs=interp_occurrences ist occs }
 
@@ -2123,6 +2123,9 @@ let () =
   Geninterp.register_interp0 wit_ref interp;
   let interp ist gl pat = (project gl, interp_intro_pattern ist (pf_env gl) pat) in
   Geninterp.register_interp0 wit_intro_pattern interp;
+  let interp ist gl pat = (project gl, interp_clause ist (pf_env gl) pat) in
+  Geninterp.register_interp0 wit_clause_dft_concl interp;
+
   let interp ist gl s = (project gl, interp_sort s) in
   Geninterp.register_interp0 wit_sort interp
 
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index d3cc6adc5..997975196 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -330,6 +330,7 @@ let () =
   Genintern.register_subst0 wit_ref subst_global_reference;
   Genintern.register_subst0 wit_intro_pattern (fun _ v -> v);
   Genintern.register_subst0 wit_tactic subst_tactic;
-  Genintern.register_subst0 wit_sort (fun _ v -> v)
+  Genintern.register_subst0 wit_sort (fun _ v -> v);
+  Genintern.register_subst0 wit_clause_dft_concl (fun _ v -> v)
 
 let _ = Hook.set Auto.extern_subst_tactic subst_tactic