diff options
| author | Matthieu Sozeau | 2015-10-01 16:24:54 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-02 15:54:13 +0200 |
| commit | b144ef5e2698932c5b2f7cdb1688a55ce4764dae (patch) | |
| tree | 36dd11b8e36397280727cb4ecb3f123b04e8633c | |
| parent | 1d01533266b247cbc32903935963674acf7c6c54 (diff) | |
Fix after rebase...
| -rw-r--r-- | toplevel/auto_ind_decl.ml | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 009e423e4f..8ac273c84f 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -764,16 +764,10 @@ let make_lb_scheme mode mind = let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in -<<<<<<< HEAD - let ctx = Evd.empty_evar_universe_context in + let ctx = Evd.make_evar_universe_context (Global.env ()) None in let side_eff = side_effect_of_mode mode in let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx lb_goal (compute_lb_tact mode (!lb_scheme_kind_aux()) ind lnamesparrec nparrec) -======= - let ctx = Evd.make_evar_universe_context (Global.env ()) None in - let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx lb_goal - (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec) ->>>>>>> Univs: fix environment handling in scheme building. in ([|ans|], ctx), eff |