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 | |
| parent | 91b82f5a7b3cff65aeadd7c8323d63bf91b5f2e1 (diff) | |
| parent | 8131e35caaacf86cd52262329ab1b0aaa1b8c5b3 (diff) | |
Merge PR#508: Optimize pending evars
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/command.ml | 8 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 2 | ||||
| -rw-r--r-- | vernac/record.ml | 2 |
3 files changed, 6 insertions, 6 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) diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 798a238c74..409676276a 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -463,7 +463,7 @@ let start_proof_com ?inference_hook kind thms hook = let t', imps' = interp_type_evars_impls ~impls env evdref t in let flags = all_and_fail_flags in let flags = { flags with use_hook = inference_hook } in - evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref); + evdref := solve_remaining_evars flags env !evdref Evd.empty; let ids = List.map RelDecl.get_name ctx in (compute_proof_name (pi1 kind) sopt, (nf_evar !evdref (it_mkProd_or_LetIn t' ctx), diff --git a/vernac/record.ml b/vernac/record.ml index 51d89f1551..288d3391bb 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -141,7 +141,7 @@ let typecheck_params_and_fields def id pl t ps nots fs = interp_fields_evars env_ar evars impls_env nots (binders_of_decls fs) in let sigma = - Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar !evars (Evd.empty,!evars) in + Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar !evars Evd.empty in let evars, nf = Evarutil.nf_evars_and_universes sigma in let arity = nf t' in let arity, evars = |