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

2 files changed, 11 insertions, 9 deletions

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