diff options
| author | Pierre-Marie Pédrot | 2017-04-07 11:50:57 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-04-07 11:50:57 +0200 |
| commit | 3a1df73d60372d1966c69450f80a66ca72cb9b44 (patch) | |
| tree | 34f2b0419b52861cb83bb42a90728161c7f792b4 /vernac/command.ml | |
| parent | d6175b9980808ff91f1299ca26a9a49a117169ca (diff) | |
| parent | 63c73f54023f53a790ef57c9afc22111b9b95412 (diff) | |
Merge branch 'master' into econstr
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 0393669d43..781bf32239 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -143,7 +143,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 = @@ -305,7 +305,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 @@ -614,7 +614,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 @@ -1174,7 +1174,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 evd isfix (List.combine fixnames fixdefs) |