diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-02-02 15:55:54 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-02-02 15:55:54 +0100 |
| commit | e6353e9ef6542b444391a46d9557ebf3a6443947 (patch) | |
| tree | 5cdc9ba397db963006d747716321c029b194eba8 /tactics | |
| parent | 1d9e15c99a90311f8e082fb39615ae1c4aee8084 (diff) | |
Reductionops.nf_* now take an environment.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 8 |
2 files changed, 5 insertions, 5 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 22073d39b..450d68436 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1583,7 +1583,7 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b = let body = mkApp (lambda_create env sigma (typ,pred_body),[|dep_pair1|]) in let expected_goal = beta_applist sigma (abst_B,List.map fst e2_list) in (* Simulate now the normalisation treatment made by Logic.mk_refgoals *) - let expected_goal = nf_betaiota sigma expected_goal in + let expected_goal = nf_betaiota env sigma expected_goal in (* Retype to get universes right *) let sigma, expected_goal_ty = Typing.type_of env sigma expected_goal in let sigma, _ = Typing.type_of env sigma body in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 4ee0a8a7b..9fded04db 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -471,7 +471,7 @@ let internal_cut_gen ?(check=true) dir replace id t = (if check && mem_named_context_val id sign then user_err (str "Variable " ++ Id.print id ++ str " is already declared."); push_named_context_val (LocalAssum (id,t)) sign,t,concl,sigma) in - let nf_t = nf_betaiota sigma t in + let nf_t = nf_betaiota env sigma t in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Refine.refine ~typecheck:false begin fun sigma -> @@ -1728,7 +1728,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind : let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - let thm_ty0 = nf_betaiota sigma (Retyping.get_type_of env sigma c) in + let thm_ty0 = nf_betaiota env sigma (Retyping.get_type_of env sigma c) in let try_apply thm_ty nprod = try let n = nb_prod_modulo_zeta sigma thm_ty - nprod in @@ -1864,7 +1864,7 @@ let explain_unable_to_apply_lemma ?loc env sigma thm innerclause = str ".")) let apply_in_once_main flags innerclause env sigma (loc,d,lbind) = - let thm = nf_betaiota sigma (Retyping.get_type_of env sigma d) in + let thm = nf_betaiota env sigma (Retyping.get_type_of env sigma d) in let rec aux clause = try progress_with_clause flags innerclause clause with e when CErrors.noncritical e -> @@ -2162,7 +2162,7 @@ let apply_type newcl args = let env = Proofview.Goal.env gl in let store = Proofview.Goal.extra gl in Refine.refine ~typecheck:false begin fun sigma -> - let newcl = nf_betaiota sigma newcl (* As in former Logic.refine *) in + let newcl = nf_betaiota env sigma newcl (* As in former Logic.refine *) in let (sigma, ev) = Evarutil.new_evar env sigma ~principal:true ~store newcl in (sigma, applist (ev, args)) |