diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 2 | ||||
| -rw-r--r-- | tactics/equality.ml | 32 | ||||
| -rw-r--r-- | tactics/evar_tactics.ml | 2 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 12 | ||||
| -rw-r--r-- | tactics/leminv.ml | 2 | ||||
| -rw-r--r-- | tactics/rewrite.ml | 18 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 8 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 |
8 files changed, 40 insertions, 40 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 67484429f2..e386728fe7 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -912,7 +912,7 @@ let prepare_hint check env init (sigma,c) = let interp_hints poly = fun h -> let f c = - let evd,c = Constrintern.interp_open_constr Evd.empty (Global.env()) c in + let evd,c = Constrintern.interp_open_constr (Global.env()) Evd.empty c in prepare_hint true (Global.env()) Evd.empty (evd,c) in let fr r = let gr = global_with_alias r in diff --git a/tactics/equality.ml b/tactics/equality.ml index 74fa77e6d2..5e94f1b3b0 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -763,7 +763,7 @@ let injectable env sigma t1 t2 = *) -(* [descend_then sigma env head dirn] +(* [descend_then env sigma head dirn] returns the number of products introduced, and the environment which is active, in the body of the case-branch given by [dirn], @@ -778,7 +778,7 @@ let injectable env sigma t1 t2 = the continuation then constructs the case-split. *) -let descend_then sigma env head dirn = +let descend_then env sigma head dirn = let IndType (indf,_) = try find_rectype env sigma (get_type_of env sigma head) with Not_found -> @@ -821,7 +821,7 @@ let descend_then sigma env head dirn = constructs a case-split on [headval], with the [dirn]-th branch giving [True], and all the rest giving False. *) -let construct_discriminator sigma env dirn c sort = +let construct_discriminator env sigma dirn c sort = let IndType(indf,_) = try find_rectype env sigma (get_type_of env sigma c) with Not_found -> @@ -848,12 +848,12 @@ let construct_discriminator sigma env dirn c sort = let ci = make_case_info env ind RegularStyle in mkCase (ci, p, c, Array.of_list brl) -let rec build_discriminator sigma env dirn c sort = function - | [] -> construct_discriminator sigma env dirn c sort +let rec build_discriminator env sigma dirn c sort = function + | [] -> construct_discriminator env sigma dirn c sort | ((sp,cnum),argnum)::l -> - let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in + let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in let newc = mkRel(cnum_nlams-argnum) in - let subval = build_discriminator sigma cnum_env dirn newc sort l in + let subval = build_discriminator cnum_env sigma dirn newc sort l in kont subval (build_coq_False (),mkSort (Prop Null)) (* Note: discrimination could be more clever: if some elimination is @@ -919,7 +919,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort = let e = next_ident_away eq_baseid (ids_of_context env) in let e_env = push_named (e,None,t) env in let discriminator = - build_discriminator sigma e_env dirn (mkVar e) sort cpath in + build_discriminator e_env sigma dirn (mkVar e) sort cpath in let sigma,(pf, absurd_term), eff = discrimination_pf env sigma e (t,t1,t2) discriminator lbeq in let pf_ty = mkArrow eqn absurd_term in @@ -1111,7 +1111,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let (a,p_i_minus_1) = match whd_beta_stack !evdref p_i with | (_sigS,[a;p]) -> (a,p) | _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type") in - let ev = Evarutil.e_new_evar evdref env a in + let ev = Evarutil.e_new_evar env evdref a in let rty = beta_applist(p_i_minus_1,[ev]) in let tuple_tail = sigrec_clausal_form (siglen-1) rty in match @@ -1161,7 +1161,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = If [zty] has no dependencies, this is simple. Otherwise, assume [zty] has free (de Bruijn) variables in,...i1 then the role of - [make_iterated_tuple sigma env (term,typ) (z,zty)] is to build the + [make_iterated_tuple env sigma (term,typ) (z,zty)] is to build the tuple [existT [xn]Pn Rel(in) .. (existT [x2]P2 Rel(i2) (existT [x1]P1 Rel(i1) z))] @@ -1200,19 +1200,19 @@ let make_iterated_tuple env sigma dflt (z,zty) = let sigma, dfltval = sig_clausal_form env sigma sort_of_zty n tuplety dflt in sigma, (tuple,tuplety,dfltval) -let rec build_injrec sigma env dflt c = function +let rec build_injrec env sigma dflt c = function | [] -> make_iterated_tuple env sigma dflt (c,type_of env sigma c) | ((sp,cnum),argnum)::l -> try - let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in + let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in let newc = mkRel(cnum_nlams-argnum) in - let sigma, (subval,tuplety,dfltval) = build_injrec sigma cnum_env dflt newc l in + let sigma, (subval,tuplety,dfltval) = build_injrec cnum_env sigma dflt newc l in sigma, (kont subval (dfltval,tuplety), tuplety,dfltval) with UserError _ -> failwith "caught" -let build_injector sigma env dflt c cpath = - let sigma, (injcode,resty,_) = build_injrec sigma env dflt c cpath in +let build_injector env sigma dflt c cpath = + let sigma, (injcode,resty,_) = build_injrec env sigma dflt c cpath in sigma, (injcode,resty) (* @@ -1289,7 +1289,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = let filter (cpath, t1', t2') = try (* arbitrarily take t1' as the injector default value *) - let sigma, (injbody,resty) = build_injector !evdref e_env t1' (mkVar e) cpath in + let sigma, (injbody,resty) = build_injector e_env !evdref t1' (mkVar e) cpath in let injfun = mkNamedLambda e t injbody in let sigma,congr = Evd.fresh_global env sigma eq.congr in let pf = applist(congr,[t;resty;injfun;t1;t2]) in diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index 33505c7fcf..7c4c9c9657 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -71,7 +71,7 @@ let let_evar name typ = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in - let sigma',evar = Evarutil.new_evar sigma env ~src typ in + let sigma',evar = Evarutil.new_evar env sigma ~src typ in Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS sigma')) (Tactics.letin_tac None name evar None Locusops.nowhere) end diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index f701918670..e4ba9a7ee5 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -269,7 +269,7 @@ let add_rewrite_hint bases ort t lcsr = let env = Global.env() and sigma = Evd.empty in let poly = Flags.is_universe_polymorphism () in let f ce = - let c, ctx = Constrintern.interp_constr sigma env ce in + let c, ctx = Constrintern.interp_constr env sigma ce in let ctx = if poly then Evd.evar_universe_context_set ctx @@ -372,7 +372,7 @@ let refine_tac {Glob_term.closure=closure;term=term} = Pretyping.ltac_uconstrs = closure.Glob_term.untyped; Pretyping.ltac_idents = closure.Glob_term.idents; } in - let update evd = Pretyping.understand_ltac flags evd env lvar tycon term in + let update evd = Pretyping.understand_ltac flags env evd lvar tycon term in Proofview.Refine.refine ~unsafe:false (fun h -> Proofview.Refine.update h update) <*> Proofview.V82.tactic (reduce refine_red_flags refine_locs) end @@ -505,7 +505,7 @@ let inTransitivity : bool * constr -> obj = (* Main entry points *) let add_transitivity_lemma left lem = - let lem',ctx (*FIXME*) = Constrintern.interp_constr Evd.empty (Global.env ()) lem in + let lem',ctx (*FIXME*) = Constrintern.interp_constr (Global.env ()) Evd.empty lem in add_anonymous_leaf (inTransitivity (left,lem')) (* Vernacular syntax *) @@ -545,8 +545,8 @@ END VERNAC COMMAND EXTEND RetroknowledgeRegister CLASSIFIED AS SIDEFF | [ "Register" constr(c) "as" retroknowledge_field(f) "by" constr(b)] -> - [ let tc,ctx = Constrintern.interp_constr Evd.empty (Global.env ()) c in - let tb,ctx(*FIXME*) = Constrintern.interp_constr Evd.empty (Global.env ()) b in + [ let tc,ctx = Constrintern.interp_constr (Global.env ()) Evd.empty c in + let tb,ctx(*FIXME*) = Constrintern.interp_constr (Global.env ()) Evd.empty b in Global.register f tc tb ] END @@ -633,7 +633,7 @@ let hResolve id c occ t gl = let t_raw = Detyping.detype true env_ids env_names sigma t in let rec resolve_hole t_hole = try - Pretyping.understand sigma env t_hole + Pretyping.understand env sigma t_hole with | Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) as e -> let loc = match Loc.get_loc e with None -> Loc.ghost | Some loc -> loc in diff --git a/tactics/leminv.ml b/tactics/leminv.ml index e9dace8581..7eb81c3f48 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -237,7 +237,7 @@ let add_inversion_lemma name env sigma t sort dep inv_op = let add_inversion_lemma_exn na com comsort bool tac = let env = Global.env () and evd = ref Evd.empty in - let c = Constrintern.interp_type_evars evd env com in + let c = Constrintern.interp_type_evars env evd com in let sigma, sort = Pretyping.interp_sort !evd comsort in try add_inversion_lemma na env sigma c sort bool tac diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 5b24facc34..6a1ac2706f 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -106,12 +106,12 @@ let cstrevars evars = snd evars let new_cstr_evar (evd,cstrs) env t = let s = Typeclasses.set_resolvable Evd.Store.empty false in - let evd', t = Evarutil.new_evar ~store:s evd env t in + let evd', t = Evarutil.new_evar ~store:s env evd t in let ev, _ = destEvar t in (evd', Evar.Set.add ev cstrs), t (** Building or looking up instances. *) -let e_new_cstr_evar evars env t = +let e_new_cstr_evar env evars t = let evd', t = new_cstr_evar !evars env t in evars := evd'; t (** Building or looking up instances. *) @@ -364,7 +364,7 @@ end) = struct (try let params, args = Array.chop (Array.length args - 2) args in let env' = Environ.push_rel_context rels env in - let evars, (evar, _) = Evarutil.new_type_evar Evd.univ_flexible sigma env' in + let evars, (evar, _) = Evarutil.new_type_evar env' sigma Evd.univ_flexible in let evars, inst = app_poly env (evars,Evar.Set.empty) rewrite_relation_class [| evar; mkApp (c, params) |] in @@ -424,7 +424,7 @@ module TypeGlobal = struct let inverse env (evd,cstrs) car rel = - let evd, (sort,_) = Evarutil.new_type_evar Evd.univ_flexible evd env in + let evd, (sort,_) = Evarutil.new_type_evar env evd Evd.univ_flexible in app_poly_check env (evd,cstrs) coq_inverse [| car ; car; sort; rel |] end @@ -1334,7 +1334,7 @@ module Strategies = let fold_glob c : 'a pure_strategy = fun state env avoid t ty cstr evars -> (* let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *) - let sigma, c = Pretyping.understand_tcc (goalevars evars) env c in + let sigma, c = Pretyping.understand_tcc env (goalevars evars) c in let unfolded = try Tacred.try_red_product env sigma c with e when Errors.noncritical e -> @@ -1595,13 +1595,13 @@ let cl_rewrite_clause l left2right occs clause gl = cl_rewrite_clause_strat strat clause gl let apply_glob_constr c l2r occs = fun () env avoid t ty cstr evars -> - let evd, c = (Pretyping.understand_tcc (goalevars evars) env c) in + let evd, c = (Pretyping.understand_tcc env (goalevars evars) c) in apply_lemma l2r (general_rewrite_unif_flags ()) (Evd.empty, (c, NoBindings)) None occs () env avoid t ty cstr (evd, cstrevars evars) let interp_glob_constr_list env sigma = List.map (fun c -> - let evd, c = Pretyping.understand_tcc sigma env c in + let evd, c = Pretyping.understand_tcc env sigma c in (evd, (c, NoBindings)), true, None) (* Syntax for rewriting with strategies *) @@ -1792,7 +1792,7 @@ let declare_projection n instance_id r = let build_morphism_signature m = let env = Global.env () in - let m,ctx = Constrintern.interp_constr Evd.empty env m in + let m,ctx = Constrintern.interp_constr env Evd.empty m in let sigma = Evd.from_env ~ctx env in let t = Typing.type_of env sigma m in let cstrs = @@ -1810,7 +1810,7 @@ let build_morphism_signature m = (fun (ty, rel) -> Option.iter (fun rel -> let default = e_app_poly env evd PropGlobal.default_relation [| ty; rel |] in - ignore(e_new_cstr_evar evd env default)) + ignore(e_new_cstr_evar env evd default)) rel) cstrs in diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index a243667a5a..9d2f8c9048 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -512,7 +512,7 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) = let trace = push_trace (loc_of_glob_constr c,LtacConstrInterp (c,vars)) ist in let (evd,c) = - catch_error trace (understand_ltac flags sigma env vars kind) c + catch_error trace (understand_ltac flags env sigma vars kind) c in (* spiwack: to avoid unnecessary modifications of tacinterp, as this function already use effect, I call [run] hoping it doesn't mess @@ -622,8 +622,8 @@ let interp_unfold ist env sigma (occs,qid) = let interp_flag ist env sigma red = { red with rConst = List.map (interp_evaluable ist env sigma) red.rConst } -let interp_constr_with_occurrences ist sigma env (occs,c) = - let (sigma,c_interp) = interp_constr ist sigma env c in +let interp_constr_with_occurrences ist env sigma (occs,c) = + let (sigma,c_interp) = interp_constr ist env sigma c in sigma , (interp_occurrences ist occs, c_interp) let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, c) = @@ -1323,7 +1323,7 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t = Pretyping.ltac_genargs = ist.lfun; } in let (sigma,c_interp) = - Pretyping.understand_ltac constr_flags sigma env vars WithoutTypeConstraint term + Pretyping.understand_ltac constr_flags env sigma vars WithoutTypeConstraint term in Ftactic.(lift (Proofview.V82.tclEVARS sigma) <*> return (Value.of_constr c_interp)) end diff --git a/tactics/tactics.ml b/tactics/tactics.ml index d24645968a..48bfeb86e4 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1449,7 +1449,7 @@ let vm_cast_no_check c gl = let exact_proof c gl = - let c,ctx = Constrintern.interp_casted_constr (project gl) (pf_env gl) c (pf_concl gl) + let c,ctx = Constrintern.interp_casted_constr (pf_env gl) (project gl) c (pf_concl gl) in tclTHEN (tclEVARUNIVCONTEXT ctx) (refine_no_check c) gl let assumption = @@ -3021,7 +3021,7 @@ let specialize_eqs id gl = | _ -> if in_eqs then acc, in_eqs, ctx, ty else - let e = e_new_evar evars (push_rel_context ctx env) t in + let e = e_new_evar (push_rel_context ctx env) evars t in aux false ((na, Some e, t) :: ctx) (mkApp (lift 1 acc, [| mkRel 1 |])) b) | t -> acc, in_eqs, ctx, ty in |