diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-26 15:03:10 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-14 13:25:56 +0200 |
| commit | c22ac10752c12bcb23402ad29a73f2d9699248a6 (patch) | |
| tree | 9a77251356af06e08c70f46235815f6a6d4c2bfb /vernac | |
| parent | e68f8c904b7ee8fee9f98f75e37ab6d01b54731f (diff) | |
Deprecate Typing.e_* functions
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comFixpoint.ml | 4 | ||||
| -rw-r--r-- | vernac/comProgramFixpoint.ml | 4 |
2 files changed, 2 insertions, 6 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 7b382dacc..85c0699ea 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -199,9 +199,7 @@ let interp_recursive ~program_mode ~cofix fixl notations = try let sigma, h_term = fix_proto sigma in let app = mkApp (h_term, [|sort; t|]) in - let _evd = ref sigma in - let res = Typing.e_solve_evars env _evd app in - !_evd, res + Typing.solve_evars env sigma app with e when CErrors.noncritical e -> sigma, t in sigma, LocalAssum (id,fixprot) :: env' diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 745f1df1d..349fc562b 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -190,9 +190,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof in sigma, mkApp (h_a_term, [| argtyp ; wf_rel ; h_e_term; prop |]) in - let _evd = ref sigma in - let def = Typing.e_solve_evars env _evd def in - let sigma = !_evd in + let sigma, def = Typing.solve_evars env sigma def in let sigma = Evarutil.nf_evar_map sigma in let def = mkApp (def, [|intern_body_lam|]) in let binders_rel = nf_evar_context sigma binders_rel in |