diff options
Diffstat (limited to 'tactics/refine.ml')
-rw-r--r-- | tactics/refine.ml | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/tactics/refine.ml b/tactics/refine.ml index 169e51467..db4c52020 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -333,23 +333,10 @@ let rec tcc_aux subst (TH (c,mm,sgp) as th) gl = (function None -> tclIDTAC | Some th -> tcc_aux subst th) sgp) gl - -(* La coercion face au but était faite auparavant dans Tacinterp *) - -let coerce_to_goal (sigma,c) gl = - let env = pf_env gl in - let evars = Evd.create_evar_defs sigma in - let j = Retyping.get_judgment_of env sigma c in - let ccl = pf_concl gl in - let (evars,j) = Coercion.inh_conv_coerce_to dummy_loc env evars j ccl in - let sigma = Evd.evars_of evars in - (sigma,Reductionops.nf_evar sigma j.Environ.uj_val) - (* Et finalement la tactique refine elle-même : *) let refine oc gl = let sigma = project gl in - let oc = coerce_to_goal oc gl in let (_gmm,c) = Evarutil.exist_to_meta sigma oc in (* Relies on Cast's put on Meta's by exist_to_meta, because it is otherwise complicated to update gmm when passing through a binder *) |