From 864fda19d046428023851ba540b82c5ca24d06a4 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 25 Apr 2018 18:08:39 +0200 Subject: Deprecate most evarutil evdref functions clear_hyps remain with no alternative --- tactics/equality.ml | 36 +++++++++++++++++++----------------- tactics/tactics.ml | 3 ++- 2 files changed, 21 insertions(+), 18 deletions(-) (limited to 'tactics') diff --git a/tactics/equality.ml b/tactics/equality.ml index b6bbd0be4..d142e10a4 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1176,34 +1176,35 @@ let minimal_free_rels_rec env sigma = let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let sigdata = find_sigma_data env sort_of_ty in - let evdref = ref (Evd.clear_metas sigma) in - let rec sigrec_clausal_form siglen p_i = + let rec sigrec_clausal_form sigma siglen p_i = if Int.equal siglen 0 then (* is the default value typable with the expected type *) let dflt_typ = unsafe_type_of env sigma dflt in try - let () = evdref := Evarconv.the_conv_x_leq env dflt_typ p_i !evdref in - let () = - evdref := Evarconv.solve_unif_constraints_with_heuristics env !evdref in - dflt + let sigma = Evarconv.the_conv_x_leq env dflt_typ p_i sigma in + let sigma = + Evarconv.solve_unif_constraints_with_heuristics env sigma in + sigma, dflt with Evarconv.UnableToUnify _ -> user_err Pp.(str "Cannot solve a unification problem.") else - let (a,p_i_minus_1) = match whd_beta_stack !evdref p_i with + let (a,p_i_minus_1) = match whd_beta_stack sigma p_i with | (_sigS,[a;p]) -> (a, p) | _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type.") in - let ev = Evarutil.e_new_evar env evdref a in + let sigma, ev = Evarutil.new_evar env sigma a in let rty = beta_applist sigma (p_i_minus_1,[ev]) in - let tuple_tail = sigrec_clausal_form (siglen-1) rty in - let evopt = match EConstr.kind !evdref ev with Evar _ -> None | _ -> Some ev in + let sigma, tuple_tail = sigrec_clausal_form sigma (siglen-1) rty in + let evopt = match EConstr.kind sigma ev with Evar _ -> None | _ -> Some ev in match evopt with | Some w -> - let w_type = unsafe_type_of env !evdref w in - if Evarconv.e_cumul env evdref w_type a then - let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in - applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) - else + let w_type = unsafe_type_of env sigma w in + begin match Evarconv.cumul env sigma w_type a with + | Some sigma -> + let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in + sigma, applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) + | None -> user_err Pp.(str "Cannot solve a unification problem.") + end | None -> (* This at least happens if what has been detected as a dependency is not one; use an evasive error message; @@ -1213,8 +1214,9 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = unsolved evars would mean not binding rel *) user_err Pp.(str "Cannot solve a unification problem.") in - let scf = sigrec_clausal_form siglen ty in - !evdref, Evarutil.nf_evar !evdref scf + let sigma = Evd.clear_metas sigma in + let sigma, scf = sigrec_clausal_form sigma siglen ty in + sigma, Evarutil.nf_evar sigma scf (* The problem is to build a destructor (a generalization of the predecessor) which, when applied to a term made of constructors diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ee76ad077..178c10815 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3840,7 +3840,8 @@ let specialize_eqs id = | _ -> if in_eqs then acc, in_eqs, ctx, ty else - let e = e_new_evar (push_rel_context ctx env) evars t in + let sigma, e = Evarutil.new_evar (push_rel_context ctx env) !evars t in + evars := sigma; aux false (LocalDef (na,e,t) :: ctx) (mkApp (lift 1 acc, [| mkRel 1 |])) b) | t -> acc, in_eqs, ctx, ty in -- cgit v1.2.3