diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-26 14:29:34 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-11 13:41:26 +0200 |
| commit | 8894e9eb35e5529966fea699014fef83e4b270bd (patch) | |
| tree | 14e790361a89a4f0b50b5e45a0e4ea9fb74a33c0 /pretyping | |
| parent | 81107b12644c78f204d0a46df520b8b2d8e72142 (diff) | |
set_solve_evars doesn't use an evar_map ref
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 13 | ||||
| -rw-r--r-- | pretyping/evarconv.mli | 2 | ||||
| -rw-r--r-- | pretyping/typing.ml | 7 |
3 files changed, 14 insertions, 8 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 2144639d5..49c429458 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1159,17 +1159,18 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = let subst = make_subst (ctxt,Array.to_list args,argoccs) in - let evdref = ref evd in - let rhs = set_holes evdref rhs subst in - let evd = !evdref in + let evd, rhs = + let evdref = ref evd in + let rhs = set_holes evdref rhs subst in + !evdref, rhs + in (* We instantiate the evars of which the value is forced by typing *) let evd,rhs = - let evdref = ref evd in - try let c = !solve_evars env_evar evdref rhs in !evdref,c + try !solve_evars env_evar evd rhs with e when Pretype_errors.precatchable_exception e -> (* Could not revert all subterms *) - raise (TypingFailed !evdref) in + raise (TypingFailed evd) in let rec abstract_free_holes evd = function | (id,idty,c,_,evsref,_,_)::l -> diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index bea3eeb2e..cdf5dd0e5 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -69,7 +69,7 @@ val second_order_matching : transparent_state -> env -> evar_map -> (** Declare function to enforce evars resolution by using typing constraints *) -val set_solve_evars : (env -> evar_map ref -> constr -> constr) -> unit +val set_solve_evars : (env -> evar_map -> constr -> evar_map * constr) -> unit type unify_fun = transparent_state -> env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result diff --git a/pretyping/typing.ml b/pretyping/typing.ml index da72d7a75..281e33e9b 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -443,4 +443,9 @@ let e_solve_evars env evdref c = (* side-effect on evdref *) nf_evar !evdref c -let _ = Evarconv.set_solve_evars (fun env evdref c -> e_solve_evars env evdref c) +let solve_evars env sigma c = + let evdref = ref sigma in + let c = e_solve_evars env evdref c in + !evdref, c + +let _ = Evarconv.set_solve_evars (fun env sigma c -> solve_evars env sigma c) |