diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/eauto.ml | 2 | ||||
| -rw-r--r-- | tactics/eqschemes.ml | 2 | ||||
| -rw-r--r-- | tactics/equality.ml | 9 | ||||
| -rw-r--r-- | tactics/hipattern.ml | 8 | ||||
| -rw-r--r-- | tactics/tactics.ml | 6 |
5 files changed, 14 insertions, 13 deletions
diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 28b5ed5811..7b323ee0ed 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -485,7 +485,7 @@ let unfold_head env sigma (ids, csts) c = true, EConstr.of_constr (Environ.constant_value_in env (cst, u)) | App (f, args) -> (match aux f with - | true, f' -> true, Reductionops.whd_betaiota sigma (mkApp (f', args)) + | true, f' -> true, Reductionops.whd_betaiota env sigma (mkApp (f', args)) | false, _ -> let done_, args' = Array.fold_left_i (fun i (done_, acc) arg -> diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 7c702eab3a..6da2248cc3 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -653,7 +653,7 @@ let fix_r2l_forward_rew_scheme (c, ctx') = (mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 1) p) (mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 2) hp) (mkLambda_or_LetIn (RelDecl.map_constr (lift 2) ind) - (EConstr.Unsafe.to_constr (Reductionops.whd_beta sigma + (EConstr.Unsafe.to_constr (Reductionops.whd_beta env sigma (EConstr.of_constr (applist (c, Context.Rel.to_extended_list mkRel 3 indargs @ [mkRel 1;mkRel 3;mkRel 2])))))))) in c', ctx' diff --git a/tactics/equality.ml b/tactics/equality.ml index e1d34af13e..31384a353c 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -423,7 +423,8 @@ let type_of_clause cls gl = match cls with let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl = Proofview.Goal.enter begin fun gl -> let evd = Proofview.Goal.sigma gl in - let isatomic = isProd evd (whd_zeta evd hdcncl) in + let env = Proofview.Goal.env gl in + let isatomic = isProd evd (whd_zeta env evd hdcncl) in let dep_fun = if isatomic then dependent else dependent_no_evar in let type_of_cls = type_of_clause cls gl in let dep = dep_proof_ok && dep_fun evd c type_of_cls in @@ -458,7 +459,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let ctype = get_type_of env sigma c in - let rels, t = decompose_prod_assum sigma (whd_betaiotazeta sigma ctype) in + let rels, t = decompose_prod_assum sigma (whd_betaiotazeta env sigma ctype) in match match_with_equality_type env sigma t with | Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *) let lft2rgt = adjust_rewriting_direction args lft2rgt in @@ -475,7 +476,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac Proofview.tclEVARMAP >>= fun sigma -> let env' = push_rel_context rels env in let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *) - match match_with_equality_type env sigma t' with + match match_with_equality_type env' sigma t' with | Some (hdcncl,args) -> let lft2rgt = adjust_rewriting_direction args lft2rgt in leibniz_rewrite_ebindings_clause cls lft2rgt tac c @@ -1214,7 +1215,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = with Evarconv.UnableToUnify _ -> user_err Pp.(str "Cannot solve a unification problem.") else - let (a,p_i_minus_1) = match whd_beta_stack sigma p_i with + let (a,p_i_minus_1) = match whd_beta_stack env sigma p_i with | (_sigS,[a;p]) -> (a, p) | _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type.") in let sigma, ev = Evarutil.new_evar env sigma a in diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 76b1c94759..5338e0eef5 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -88,9 +88,9 @@ let is_lax_conjunction = function let prod_assum sigma t = fst (decompose_prod_assum sigma t) (* whd_beta normalize the types of arguments in a product *) -let rec whd_beta_prod sigma c = match EConstr.kind sigma c with - | Prod (n,t,c) -> mkProd (n,Reductionops.whd_beta sigma t,whd_beta_prod sigma c) - | LetIn (n,d,t,c) -> mkLetIn (n,d,t,whd_beta_prod sigma c) +let rec whd_beta_prod env sigma c = match EConstr.kind sigma c with + | Prod (n,t,c) -> mkProd (n,Reductionops.whd_beta env sigma t,whd_beta_prod env sigma c) + | LetIn (n,d,t,c) -> mkLetIn (n,d,t,whd_beta_prod env sigma c) | _ -> c let match_with_one_constructor env sigma style onlybinary allow_rec t = @@ -119,7 +119,7 @@ let match_with_one_constructor env sigma style onlybinary allow_rec t = else let ctx, cty = mip.mind_nf_lc.(0) in let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in - let ctyp = whd_beta_prod sigma + let ctyp = whd_beta_prod env sigma (Termops.prod_applist_assum sigma (Context.Rel.length mib.mind_params_ctxt) cty args) in let cargs = List.map RelDecl.get_type (prod_assum sigma ctyp) in if not (is_lax_conjunction style) || has_nodep_prod env sigma ctyp then diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e4809332c5..d0a13a8a40 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1319,7 +1319,7 @@ let cut c = let r = Sorts.relevance_of_sort s in let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_set_of_hyps gl) in (* Backward compat: normalize [c]. *) - let c = if normalize_cut then local_strong whd_betaiota sigma c else c in + let c = if normalize_cut then strong whd_betaiota env sigma c else c in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Refine.refine ~typecheck:false begin fun h -> let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c r (Vars.lift 1 concl)) in @@ -1607,7 +1607,7 @@ let make_projection env sigma params cstr sign elim i n c u = noccur_between sigma 1 (n-i-1) t (* to avoid surprising unifications, excludes flexible projection types or lambda which will be instantiated by Meta/Evar *) - && not (isEvar sigma (fst (whd_betaiota_stack sigma t))) + && not (isEvar sigma (fst (whd_betaiota_stack env sigma t))) && (accept_universal_lemma_under_conjunctions () || not (isRel sigma t)) then let t = lift (i+1-n) t in @@ -3025,7 +3025,7 @@ let specialize (c,lbind) ipat = let flags = { (default_unify_flags ()) with resolve_evars = true } in let clause = clenv_unify_meta_types ~flags clause in let sigma = clause.evd in - let (thd,tstack) = whd_nored_stack sigma (clenv_value clause) in + let (thd,tstack) = whd_nored_stack env sigma (clenv_value clause) in (* The completely applied term is (thd tstack), but tstack may contain unsolved metas, so now we must reabstract them args with there name to have |