- Added support for subterm matching in SearchAbout.

- Backtrack on precise unfolding of "iff" in "tauto": it has effects on
  the naming of hypotheses (especially when doing "case H" with H of
  type "{x|P<->Q}" since not unfolding will eventually introduce a name
  "i" while unfolding will eventually introduce a name "a" (deep sigh).
- Miscellaneous (error when a plugin is missing, doc hnf, standardization
  of names manipulating type constr_pattern, ...).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11725 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 43 insertions, 26 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 0dd90246d..ec3a8d6c9 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -581,7 +581,7 @@ let add_hints local dbnames0 h =
         add_resolves env sigma lcons local dbnames in
       List.iter add_one lqid
   | HintsExtern (pri, patcom, tacexp) ->
-      let pat =	Option.map (Constrintern.interp_constrpattern Evd.empty (Global.env())) patcom in
+      let pat =	Option.map (Constrintern.intern_constr_pattern Evd.empty (Global.env())) patcom in
       let tacexp = !forward_intern_tac (match pat with None -> [] | Some (l, _) -> l) tacexp in
       add_externs pri pat tacexp local dbnames
   | HintsDestruct(na,pri,loc,pat,code) ->
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 6622ccb60..b7929b29a 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -249,7 +249,7 @@ let add_destructor_hint local na loc pat pri code =
 	  errorlabstrm "add_destructor_hint"
           (str "The tactic should be a function of the hypothesis name.") end
   in
-  let (_,pat) = Constrintern.interp_constrpattern Evd.empty (Global.env()) pat
+  let (_,pat) = Constrintern.intern_constr_pattern Evd.empty (Global.env()) pat
   in
   let pat = match loc with
     | HypLocation b ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index bf0534167..568b6ea42 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -615,18 +615,15 @@ let intern_inversion_strength lf ist = function
 let intern_hyp_location ist (((b,occs),id),hl) =
   (((b,List.map (intern_or_var ist) occs),intern_hyp_or_metaid ist id), hl)
 
-let interp_constrpattern_gen sigma env ?(as_type=false) ltacvar c =
-  let c = intern_gen as_type ~allow_patvar:true ~ltacvars:(ltacvar,[])
-                     sigma env c in
-  pattern_of_rawconstr c
-
 (* Reads a pattern *)
 let intern_pattern sigma env ?(as_type=false) lfun = function
   | Subterm (b,ido,pc) ->
-      let (metas,pat) = interp_constrpattern_gen sigma env lfun pc in
+      let ltacvars = (lfun,[]) in
+      let (metas,pat) = intern_constr_pattern sigma env ~ltacvars pc in
       ido, metas, Subterm (b,ido,pat)
   | Term pc ->
-      let (metas,pat) = interp_constrpattern_gen sigma env ~as_type lfun pc  in
+      let ltacvars = (lfun,[]) in
+      let (metas,pat) = intern_constr_pattern sigma env ~as_type ~ltacvars pc in
       None, metas, Term pat
 
 let intern_constr_may_eval ist = function
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c43f829fd..44f07d37b 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1129,12 +1129,29 @@ let intro_or_and_pattern loc b ll l' tac =
 	nv (Array.of_list ll))
       gl)
 
-let clear_if_atomic l2r id gl =
-  let eq = pf_type_of gl (mkVar id) in
-  let (_,lhs,rhs) = snd (find_eq_data_decompose eq) in
-  if l2r & isVar lhs then tclTRY (clear [destVar lhs;id]) gl
-  else if not l2r & isVar rhs then tclTRY (clear [destVar rhs;id]) gl
-  else tclIDTAC gl
+let rewrite_hyp l2r id gl =
+  let rew_on l2r =
+    !forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) in
+  let clear_var_and_eq c =
+    tclTRY (tclTHEN (clear [id]) (tclTRY (clear [destVar c]))) in
+  let t = pf_whd_betadeltaiota gl (pf_type_of gl (mkVar id)) in
+  (* TODO: detect setoid equality? better detect the different equalities *)
+  match match_with_equality_type t with
+  | Some (hdcncl,[_;lhs;rhs]) ->
+      if l2r & isVar lhs & not (occur_var (pf_env gl) (destVar lhs) rhs) then
+	tclTHEN (rew_on l2r allClauses) (clear_var_and_eq lhs) gl
+      else if not l2r & isVar rhs & not (occur_var (pf_env gl) (destVar rhs) lhs) then
+	tclTHEN (rew_on l2r allClauses) (clear_var_and_eq rhs) gl
+      else
+	tclTHEN (rew_on l2r onConcl) (tclTRY (clear [id])) gl
+  | Some (hdcncl,[c]) ->
+      let l2r = not l2r in (* equality of the form eq_true *)
+      if isVar c then
+	tclTHEN (rew_on l2r allClauses) (clear_var_and_eq c) gl
+      else
+	tclTHEN (rew_on l2r onConcl) (tclTRY (clear [id])) gl
+  | _ ->
+      error "Cannot find a known equation."
 
 let rec explicit_intro_names = function
 | (_, IntroIdentifier id) :: l ->
@@ -1181,11 +1198,9 @@ let rec intros_patterns b avoid thin destopt = function
       tclTHEN 
         (intro_gen loc (IntroAvoid(avoid@explicit_intro_names l)) no_move true)
         (onLastHyp (fun id ->
-	  tclTHENLIST [ 
-	    !forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings)
-	      allClauses;
-	    clear_if_atomic l2r id;
-	    intros_patterns b avoid thin destopt l ]))
+	  tclTHEN
+	    (rewrite_hyp l2r id)
+	    (intros_patterns b avoid thin destopt l)))
   | [] -> clear_wildcards thin
 
 let intros_pattern = intros_patterns false [] []
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 3d85f6560..1c75059b8 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -234,13 +234,18 @@ let rec tauto_intuit t_reduce solver ist =
     ||
     $t_solver
    ) >>
-    
+
+  (* The unfolding of "iff" below is a priori too strong since it
+     reduces all occurrences in subterms even if not necessary to do
+     so. However we cannot renounce to them (even with iff dealt with
+     in "simplif") w/o breaking some intro naming. This is because, a
+     "and" or an "iff" can arrive in the scope of an inductive type,
+     say "{x:A|P x}" and "case"ing on a such an hypothesis will name P
+     x "a" or "i" depending on whether "P" is an "and" or a "iff".
+     (idem for "not" if "simplif" has a primitive treatment *)
+
 let reduction_not _ist =
- <:tactic<repeat 
-  match goal with 
-  | |- _     => progress unfold Coq.Init.Logic.not
-  | H:_ |- _ => progress unfold Coq.Init.Logic.not in H
-  end >>
+ <:tactic< unfold Coq.Init.Logic.not, Coq.Init.Logic.iff in * >>
 
 let t_reduction_not = tacticIn reduction_not