diff options
| author | Maxime Dénès | 2017-04-06 18:02:18 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-06 18:02:18 +0200 |
| commit | 97b14fa4507d1713213a3dff70a3ddd413cd4d16 (patch) | |
| tree | 77951cd3c8840e01fc85e67010f4abd0925e3cb4 /vernac/command.ml | |
| parent | 91b82f5a7b3cff65aeadd7c8323d63bf91b5f2e1 (diff) | |
| parent | 8131e35caaacf86cd52262329ab1b0aaa1b8c5b3 (diff) | |
Merge PR#508: Optimize pending evars
Diffstat (limited to 'vernac/command.ml')
| -rw-r--r-- | vernac/command.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/vernac/command.ml b/vernac/command.ml index 8244ee5346..6eb7037f84 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -139,7 +139,7 @@ let interp_definition pl bl p red_option c ctypopt = red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, pl, imps let check_definition (ce, evd, _, imps) = - check_evars_are_solved (Global.env ()) evd (Evd.empty,evd); + check_evars_are_solved (Global.env ()) evd Evd.empty; ce let warn_local_declaration = @@ -299,7 +299,7 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l = ((env,ienv),((is_coe,idl),t,imps))) (env,empty_internalization_env) l in - let evd = solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref) in + let evd = solve_remaining_evars all_and_fail_flags env !evdref Evd.empty in (* The universe constraints come from the whole telescope. *) let evd = Evd.nf_constraints evd in let ctx = Evd.universe_context_set evd in @@ -604,7 +604,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = () in (* Try further to solve evars, and instantiate them *) - let sigma = solve_remaining_evars all_and_fail_flags env_params !evdref (Evd.empty,!evdref) in + let sigma = solve_remaining_evars all_and_fail_flags env_params !evdref Evd.empty in evdref := sigma; (* Compute renewed arities *) let nf,_ = e_nf_evars_and_universes evdref in @@ -1142,7 +1142,7 @@ let interp_recursive isfix fixl notations = (env,rec_sign,all_universes,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxnames fiximps fixannots let check_recursive isfix env evd (fixnames,fixdefs,_) = - check_evars_are_solved env evd (Evd.empty,evd); + check_evars_are_solved env evd Evd.empty; if List.for_all Option.has_some fixdefs then begin let fixdefs = List.map Option.get fixdefs in check_mutuality env isfix (List.combine fixnames fixdefs) |