Add the ability to declare [Hint Extern]'s with no pattern.

This permits to create a database [relations] in [RelationClasses] with
a single extern tactic in it that tries to apply [reflexivity] or
[symmetry]. This is then automatically used in [auto with *] and repair
backward compatibility. The previous commit broke some scripts which were
using [intuition] to do (setoid) [reflexivity] or [symmetry]: this
worked only by accident, because the hint database of typeclasses was
used. Overrall, this also allows to put a bunch of
always-applicable, related tactics in some database or to use
[Hint Extern] but match only on hypotheses.


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

4 files changed, 8 insertions, 7 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 323385233..2eb2c3812 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -76,7 +76,7 @@ and ct_COMMAND =
   | CT_go of ct_INT_OR_LOCN
   | CT_guarded
   | CT_hint_destruct of ct_ID * ct_INT * ct_DESTRUCT_LOCATION * ct_FORMULA * ct_TACTIC_COM * ct_ID_LIST
-  | CT_hint_extern of ct_INT * ct_FORMULA * ct_TACTIC_COM * ct_ID_LIST
+  | CT_hint_extern of ct_INT * ct_FORMULA_OPT * ct_TACTIC_COM * ct_ID_LIST
   | CT_hintrewrite of ct_ORIENTATION * ct_FORMULA_NE_LIST * ct_ID * ct_TACTIC_COM
   | CT_hints of ct_ID * ct_ID_NE_LIST * ct_ID_LIST
   | CT_hints_immediate of ct_FORMULA_NE_LIST * ct_ID_LIST
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index dcea487a9..ddedbb325 100644
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -190,8 +190,7 @@ and e_my_find_search db_list local_db hdc concl =
                tclTHEN (unify_e_resolve (term,cl)) 
 		 (e_trivial_fail_db db_list local_db)
 	   | Unfold_nth c -> unfold_in_concl [all_occurrences,c]
-	   | Extern tacast -> Auto.conclPattern concl 
-	       (Option.get p) tacast
+	   | Extern tacast -> Auto.conclPattern concl p tacast
        in 
        (free_try tac,fmt_autotactic t))
        (*i
@@ -406,8 +405,7 @@ and my_find_search db_list local_db hdc concl =
 		(unify_resolve st (term,cl)) 
 		(trivial_fail_db db_list local_db)
 	  | Unfold_nth c -> unfold_in_concl [all_occurrences,c]
-	  | Extern tacast -> 
-	      conclPattern concl (Option.get p) tacast))
+	  | Extern tacast -> conclPattern concl p tacast))
     tacl
 
 and trivial_resolve db_list local_db cl = 
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 551ad3a33..946090099 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -246,7 +246,7 @@ and fCOMMAND = function
    fNODE "hint_destruct" 6
 | CT_hint_extern(x1, x2, x3, x4) ->
    fINT x1 ++
-   fFORMULA x2 ++
+   fFORMULA_OPT x2 ++
    fTACTIC_COM x3 ++
    fID_LIST x4 ++
    fNODE "hint_extern" 4
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 0516bd551..11d8d7a0b 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1751,7 +1751,10 @@ let rec xlate_vernac =
 	     CT_hints(CT_ident "Constructors",
 		      CT_id_ne_list(n1, names), dblist)
 	| HintsExtern (n, c, t) ->
-	    CT_hint_extern(CT_int n, xlate_formula c, xlate_tactic t, dblist)
+	    let pat = match c with 
+	      | None -> CT_coerce_ID_OPT_to_FORMULA_OPT (CT_coerce_NONE_to_ID_OPT CT_none)
+	      | Some c -> CT_coerce_FORMULA_to_FORMULA_OPT (xlate_formula c) 
+	    in CT_hint_extern(CT_int n, pat, xlate_tactic t, dblist)
         | HintsImmediate l -> 
 	 let f1, formulas = match List.map xlate_formula l with
 	     a :: tl -> a, tl