aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-05-17 17:43:37 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-05-17 17:43:37 +0200
commitb0cf6c4042ed8e91c6f7081a6f0c4b83ec9407c2 (patch)
tree7f0cd1ed2217f826c0d64f6a0fa700f506dd8e86 /vernac
parent78c8d75e38844cb88c551881112e10728962dc2d (diff)
parent9f175bbeb19175a1e422225986f139e8f1a1b56c (diff)
Merge PR #7359: Reduce usage of evar_map references
Diffstat (limited to 'vernac')
-rw-r--r--vernac/comFixpoint.ml4
-rw-r--r--vernac/comProgramFixpoint.ml4
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