diff options
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 518d2f604..40c4cfaa4 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -12,7 +12,7 @@ open Pp open CErrors open Util open Names -open Term +open Constr open Libnames open Globnames open Termops @@ -416,7 +416,7 @@ exception Partial reduction is solved by the expanded fix term. *) let solve_arity_problem env sigma fxminargs c = let evm = ref sigma in - let set_fix i = evm := Evd.define i (Constr.mkVar vfx) !evm in + let set_fix i = evm := Evd.define i (mkVar vfx) !evm in let rec check strict c = let c' = whd_betaiotazeta sigma c in let (h,rcargs) = decompose_app_vect sigma c' in @@ -558,7 +558,7 @@ let match_eval_ref_value env sigma constr stack = else None | Proj (p, c) when not (Projection.unfolded p) -> - reduction_effect_hook env sigma (EConstr.to_constr sigma constr) + reduction_effect_hook env sigma (EConstr.to_constr ~abort_on_undefined_evars:false sigma constr) (lazy (EConstr.to_constr sigma (applist (constr,stack)))); if is_evaluable env (EvalConstRef (Projection.constant p)) then Some (mkProj (Projection.unfold p, c)) @@ -641,7 +641,7 @@ let whd_nothing_for_iota env sigma s = | _ -> s) | Evar ev -> s | Meta ev -> - (try whrec (EConstr.of_constr (Evd.meta_value sigma ev), stack) + (try whrec (Evd.meta_value sigma ev, stack) with Not_found -> s) | Const (const, u) when is_transparent_constant full_transparent_state const -> let u = EInstance.kind sigma u in @@ -1279,7 +1279,7 @@ let reduce_to_ref_gen allow_product env sigma ref t = error_cannot_recognize ref | _ -> try - if eq_gr (fst (global_of_constr sigma c)) ref + if GlobRef.equal (fst (global_of_constr sigma c)) ref then it_mkProd_or_LetIn t l else raise Not_found with Not_found -> |