diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-21 12:13:05 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:34 +0100 |
| commit | 0cdb7e42f64674e246d4e24e3c725e23ceeec6bd (patch) | |
| tree | 101bd3bc2e05eb52bfc142587d425f8920671b25 /pretyping/evarsolve.ml | |
| parent | e09f3b44bb381854b647a6d9debdeddbfc49177e (diff) | |
Reductionops now return EConstrs.
Diffstat (limited to 'pretyping/evarsolve.ml')
| -rw-r--r-- | pretyping/evarsolve.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 65b6d287d..27436fdd8 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -149,7 +149,7 @@ let recheck_applications conv_algo env evdref t = let argsty = Array.map (fun x -> aux env x; EConstr.of_constr (Retyping.get_type_of env !evdref x)) args in let rec aux i ty = if i < Array.length argsty then - match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref ty)) with + match EConstr.kind !evdref (whd_all env !evdref ty) with | Prod (na, dom, codom) -> (match conv_algo env !evdref Reduction.CUMUL argsty.(i) dom with | Success evd -> evdref := evd; @@ -814,7 +814,7 @@ let rec do_projection_effects define_fun env ty evd = function let evd = Evd.define evk (Constr.mkVar id) evd in (* TODO: simplify constraints involving evk *) let evd = do_projection_effects define_fun env ty evd p in - let ty = EConstr.of_constr (whd_all env evd (Lazy.force ty)) in + let ty = whd_all env evd (Lazy.force ty) in if not (isSort evd ty) then (* Don't try to instantiate if a sort because if evar_concl is an evar it may commit to a univ level which is not the right @@ -1494,7 +1494,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1) imitate envk t in - let rhs = EConstr.of_constr (whd_beta evd rhs) (* heuristic *) in + let rhs = whd_beta evd rhs (* heuristic *) in let fast rhs = let filter_ctxt = evar_filtered_context evi in let names = ref Idset.empty in @@ -1576,7 +1576,7 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs = raise e | OccurCheckIn (evd,rhs) -> (* last chance: rhs actually reduces to ev *) - let c = EConstr.of_constr (whd_all env evd rhs) in + let c = whd_all env evd rhs in match EConstr.kind evd c with | Evar (evk',argsv2) when Evar.equal evk evk' -> solve_refl (fun env sigma pb c c' -> is_fconv pb env sigma c c') @@ -1637,7 +1637,7 @@ let reconsider_conv_pbs conv_algo evd = (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *) let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1),t2) = try - let t2 = EConstr.of_constr (whd_betaiota evd t2) in (* includes whd_evar *) + let t2 = whd_betaiota evd t2 in (* includes whd_evar *) let evd = evar_define conv_algo ~choose env evd pbty ev1 t2 in reconsider_conv_pbs conv_algo evd with |