Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tactiques d'appliquer une éventuelle coercion vers le but

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

2 files changed, 24 insertions, 16 deletions

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 6ef79ea75..fd8efc5f9 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -158,8 +158,17 @@ END
 
 open Refine
 
+let coerce_to_goal tac (sigma,c) gl =
+  let env = Tacmach.pf_env gl in
+  let evars = Evd.create_evar_defs sigma in
+  let j = Retyping.get_judgment_of env sigma c in
+  let ccl = Tacmach.pf_concl gl in
+  let (evars,j) = Coercion.inh_conv_coerce_to Util.dummy_loc env evars j ccl in
+  let sigma = Evd.evars_of evars in
+  tac (sigma,Reductionops.nf_evar sigma j.Environ.uj_val) gl
+
 TACTIC EXTEND Refine
-  [ "Refine" castedopenconstr(c) ] -> [ refine c ]
+  [ "Refine" openconstr(c) ] -> [ coerce_to_goal refine c ]
 END
 
 let refine_tac = h_refine
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 5a33f89f3..3c4130e79 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -885,9 +885,9 @@ and intern_genarg ist x =
       in_gen globwit_red_expr (intern_redexp ist (out_gen rawwit_red_expr x))
   | TacticArgType ->
       in_gen globwit_tactic (intern_tactic ist (out_gen rawwit_tactic x))
-  | CastedOpenConstrArgType ->
-      in_gen globwit_casted_open_constr 
-        (intern_constr ist (out_gen rawwit_casted_open_constr x))
+  | OpenConstrArgType ->
+      in_gen globwit_open_constr 
+        ((),intern_constr ist (snd (out_gen rawwit_open_constr x)))
   | ConstrWithBindingsArgType ->
       in_gen globwit_constr_with_bindings
         (intern_constr_with_bindings ist (out_gen rawwit_constr_with_bindings x))
@@ -1194,20 +1194,19 @@ let interp_casted_constr ocl ist sigma env (c,ce) =
 let interp_constr ist sigma env c =
   interp_casted_constr None ist sigma env c
 
-(* Interprets an open constr expression casted by the current goal *)
-let pf_interp_casted_openconstr ist gl (c,ce) =
+(* Interprets an open constr expression *)
+let pf_interp_openconstr ist gl (c,ce) =
   let sigma = project gl in
   let env = pf_env gl in
   let (ltacvars,l) = constr_list ist env in
   let typs = retype_list sigma env ltacvars in
-  let ocl = Some (pf_concl gl) in
   match ce with
   | None ->
-      Pretyping.understand_gen_tcc sigma env typs ocl c
+      Pretyping.understand_gen_tcc sigma env typs None c
     (* If at toplevel (ce<>None), the error can be due to an incorrect
        context at globalization time: we retype with the now known
        intros/lettac/inversion hypothesis names *)
-  | Some c -> interp_openconstr_gen sigma env (ltacvars,l) c ocl
+  | Some c -> interp_openconstr_gen sigma env (ltacvars,l) c None
 
 (* Interprets a constr expression *)
 let pf_interp_constr ist gl =
@@ -1586,9 +1585,9 @@ and interp_genarg ist goal x =
   | RedExprArgType ->
       in_gen wit_red_expr (pf_redexp_interp ist goal (out_gen globwit_red_expr x))
   | TacticArgType -> in_gen wit_tactic (out_gen globwit_tactic x)
-  | CastedOpenConstrArgType ->
-      in_gen wit_casted_open_constr 
-        (pf_interp_casted_openconstr ist goal (out_gen globwit_casted_open_constr x))
+  | OpenConstrArgType ->
+      in_gen wit_open_constr 
+        (pf_interp_openconstr ist goal (snd (out_gen globwit_open_constr x)))
   | ConstrWithBindingsArgType ->
       in_gen wit_constr_with_bindings
         (interp_constr_with_bindings ist goal (out_gen globwit_constr_with_bindings x))
@@ -1801,7 +1800,7 @@ and interp_atomic ist gl = function
 	val_interp ist gl (out_gen globwit_tactic x)
     | StringArgType | BoolArgType
     | QuantHypArgType | RedExprArgType 
-    | CastedOpenConstrArgType | ConstrWithBindingsArgType | BindingsArgType 
+    | OpenConstrArgType | ConstrWithBindingsArgType | BindingsArgType 
     | ExtraArgType _ | List0ArgType _ | List1ArgType _ | OptArgType _ | PairArgType _ 
 	-> error "This generic type is not supported in alias"
     in
@@ -2092,9 +2091,9 @@ and subst_genarg subst (x:glob_generic_argument) =
       in_gen globwit_red_expr (subst_redexp subst (out_gen globwit_red_expr x))
   | TacticArgType ->
       in_gen globwit_tactic (subst_tactic subst (out_gen globwit_tactic x))
-  | CastedOpenConstrArgType ->
-      in_gen globwit_casted_open_constr 
-        (subst_rawconstr subst (out_gen globwit_casted_open_constr x))
+  | OpenConstrArgType ->
+      in_gen globwit_open_constr 
+        ((),subst_rawconstr subst (snd (out_gen globwit_open_constr x)))
   | ConstrWithBindingsArgType ->
       in_gen globwit_constr_with_bindings
         (subst_raw_with_bindings subst (out_gen globwit_constr_with_bindings x))