Interpret patterns for hypotheses types in match goal in type_scope (if not a

context [] pattern). May break some user contribs...
Rename clsubstitute to substitute.


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

6 files changed, 25 insertions, 19 deletions

diff --git a/CHANGES b/CHANGES
index 2c39bb8d61..8b20786822 100644
--- a/CHANGES
+++ b/CHANGES
@@ -137,6 +137,7 @@ Tactics
 - Tactic apply now able to reason modulo unfolding of constants
   (possible source of incompatibility in situations where apply may fail, 
   e.g. as argument of a try or a repeat and in a ltac function).
+- Pattern for hypotheses types in match goal are now interpreted in type_scope.
 
 Type Classes
 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 4f740f8652..dd93d511c9 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -332,7 +332,9 @@ let resolve_one_typeclass env gl =
   let gls = { it = [ Evd.make_evar (Environ.named_context_val env) gl ] ; sigma = Evd.empty } in
   let valid x = raise (FoundTerm (fst (Refiner.extract_open_proof Evd.empty (List.hd x)))) in
   let gls', valid' = full_eauto ~tac:tclIDTAC false (true, 15) [] (gls, valid) in
-    try ignore(valid' []); assert false with FoundTerm t -> t
+    try ignore(valid' []); assert false with FoundTerm t -> 
+      let term = Evarutil.nf_evar (sig_sig gls') t in
+	if occur_existential term then raise Not_found else term
 
 let has_undefined p evd =
   Evd.fold (fun ev evi has -> has ||
@@ -890,10 +892,10 @@ let clsubstitute o c =
       (fun cl -> 
 	match cl with
 	  | Some ((_,id),_) when is_tac id -> tclIDTAC
-	  | _ -> cl_rewrite_clause c o [] cl)
+	  | _ -> tclTRY (cl_rewrite_clause c o [] cl))
 
-TACTIC EXTEND map_tac
-| [ "clsubstitute" orient(o) constr(c) ] -> [ clsubstitute o c ]
+TACTIC EXTEND substitute
+| [ "substitute" orient(o) constr(c) ] -> [ clsubstitute o c ]
 END
 
 let pr_debug _prc _prlc _prt b =
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index b7a65ab617..536b5ebbdf 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -567,18 +567,18 @@ let intern_inversion_strength lf ist = function
 let intern_hyp_location ist ((occs,id),hl) =
   ((List.map (intern_or_var ist) occs,intern_hyp ist (skip_metaid id)), hl)
 
-let interp_constrpattern_gen sigma env ltacvar c =
-  let c = intern_gen false ~allow_patvar:true ~ltacvars:(ltacvar,[])
+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 lfun = function
+let intern_pattern sigma env ?(as_type=false) lfun = function
   | Subterm (ido,pc) ->
       let (metas,pat) = interp_constrpattern_gen sigma env lfun pc in
       ido, metas, Subterm (ido,pat)
   | Term pc ->
-      let (metas,pat) = interp_constrpattern_gen sigma env lfun pc  in
+      let (metas,pat) = interp_constrpattern_gen sigma env ~as_type lfun pc  in
       None, metas, Term pat
 
 let intern_constr_may_eval ist = function
@@ -609,7 +609,7 @@ let extern_request ch req gl la =
 (* Reads the hypotheses of a Match Context rule *)
 let rec intern_match_context_hyps sigma env lfun = function
   | (Hyp ((_,na) as locna,mp))::tl ->
-      let ido, metas1, pat = intern_pattern sigma env lfun mp in
+      let ido, metas1, pat = intern_pattern sigma env ~as_type:true lfun mp in
       let lfun, metas2, hyps = intern_match_context_hyps sigma env lfun tl in
       let lfun' = name_cons na (Option.List.cons ido lfun) in
       lfun', metas1@metas2, Hyp (locna,pat)::hyps
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index d0c9991964..00519ecf40 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -66,20 +66,20 @@ Open Local Scope equiv_scope.
 
 (** Use the [clsubstitute] command which substitutes an equality in every hypothesis. *)
 
-Ltac clsubst H := 
+Ltac setoid_subst H := 
   match type of H with
-    ?x === ?y => clsubstitute H ; clear H x
+    ?x === ?y => substitute H ; clear H x
   end.
 
-Ltac clsubst_nofail :=
+Ltac setoid_subst_nofail :=
   match goal with
-    | [ H : ?x === ?y |- _ ] => clsubst H ; clsubst_nofail
+    | [ H : ?x === ?y |- _ ] => setoid_subst H ; setoid_subst_nofail
     | _ => idtac
   end.
   
 (** [subst*] will try its best at substituting every equality in the goal. *)
 
-Tactic Notation "clsubst" "*" := clsubst_nofail.
+Tactic Notation "subst" "*" := subst_no_fail ; setoid_subst_nofail.
 
 Lemma nequiv_equiv_trans : forall [ Equivalence A ] (x y z : A), x =/= y -> y === z -> x =/= z.
 Proof with auto.
@@ -99,9 +99,10 @@ Qed.
 
 Ltac equiv_simplify_one :=
   match goal with
-    | [ H : (?x === ?x)%type |- _ ] => clear H
-    | [ H : (?x === ?y)%type |- _ ] => clsubst H
-    | [ |- (?x =/= ?y)%type ] => let name:=fresh "Hneq" in intro name
+    | [ H : ?x === ?x |- _ ] => clear H
+    | [ H : ?x === ?y |- _ ] => setoid_subst H
+    | [ |- ?x =/= ?y ] => let name:=fresh "Hneq" in intro name
+    | [ |- ~ ?x === ?y ] => let name:=fresh "Hneq" in intro name
   end.
 
 Ltac equiv_simplify := repeat equiv_simplify_one.
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index e64cbd12c5..d4da4b8df4 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -74,7 +74,7 @@ Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) :
 
 Ltac clsubst H := 
   match type of H with
-    ?x == ?y => clsubstitute H ; clear H x
+    ?x == ?y => substitute H ; clear H x
   end.
 
 Ltac clsubst_nofail :=
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index df2393ace2..f31115d99e 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -87,11 +87,13 @@ Ltac clear_dups := repeat clear_dup.
 
 (** A non-failing subst that substitutes as much as possible. *)
 
-Tactic Notation "subst" "*" :=
+Ltac subst_no_fail :=
   repeat (match goal with 
             [ H : ?X = ?Y |- _ ] => subst X || subst Y                  
           end).
 
+Tactic Notation "subst" "*" := subst_no_fail.
+
 (** Tactical [on_call f tac] applies [tac] on any application of [f] in the hypothesis or goal. *)
 Ltac on_call f tac :=
   match goal with