diff options
| -rw-r--r-- | pretyping/clenv.ml | 10 | ||||
| -rw-r--r-- | pretyping/clenv.mli | 4 | ||||
| -rw-r--r-- | tactics/setoid_replace.ml | 24 |
3 files changed, 18 insertions, 20 deletions
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index d79910c99..b18034b50 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -127,6 +127,16 @@ let clenv_environments_evars env evd bound c = in clrec (evd,[]) bound c +let clenv_conv_leq env sigma t c bound = + let ty = Retyping.get_type_of env sigma c in + let evd = Evd.create_evar_defs sigma in + let evars,args,_ = clenv_environments_evars env evd (Some bound) ty in + let evars = Evarconv.the_conv_x_leq env t (applist (c,args)) evars in + let evars,_ = Evarconv.consider_remaining_unif_problems env evars in + let args = List.map (whd_evar (Evd.evars_of evars)) args in + check_evars env sigma evars (applist (c,args)); + args + let mk_clenv_from_n gls n (c,cty) = let evd = create_evar_defs gls.sigma in let (env,args,concl) = clenv_environments evd n cty in diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index 98950458e..b855ee7e0 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.mli @@ -125,6 +125,10 @@ val clenv_environments : val clenv_environments_evars : env -> evar_defs -> int option -> types -> evar_defs * constr list * types +(* [clenv_conv_leq env sigma t c n] looks for c1...cn s.t. [t <= c c1...cn] *) +val clenv_conv_leq : + env -> evar_map -> types -> constr -> int -> constr list + (* if the clause is a product, add an extra meta for this product *) exception NotExtensibleClause val clenv_push_prod : clausenv -> clausenv diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 5da0bb047..99cf25779 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -727,26 +727,10 @@ let unify_relation_carrier_with_type env rel t = if rel.rel_quantifiers_no = 0 && is_conv env Evd.empty rel.rel_a t then [||] else - begin - let evars,args,instantiated_rel_a = - let ty = Typing.type_of env Evd.empty rel.rel_a in - let evd = Evd.create_evar_defs Evd.empty in - let evars,args,concl = - Clenv.clenv_environments_evars env evd - (Some rel.rel_quantifiers_no) ty - in - evars, args, - nf_betaiota - (match args with [] -> rel.rel_a | _ -> applist (rel.rel_a,args)) - in - let evars' = - w_unify true (*??? or false? *) env Reduction.CONV (*??? or cumul? *) - ~mod_delta:true (*??? or true? *) t instantiated_rel_a evars in - let args' = - List.map (Reductionops.nf_evar (Evd.evars_of evars')) args - in - Array.of_list args' - end + let args = + Clenv.clenv_conv_leq env Evd.empty t rel.rel_a rel.rel_quantifiers_no + in + Array.of_list args in apply_to_relation args rel |