diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/hints.ml | 6 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 10 |
2 files changed, 8 insertions, 8 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 5630d20b5d..6250886821 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -677,7 +677,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) = match kind_of_term cty with | Prod _ -> failwith "make_exact_entry" | _ -> - let pat = pi3 (Patternops.pattern_of_constr env sigma cty) in + let pat = Patternops.pattern_of_constr env sigma cty in let hd = try head_pattern_bound pat with BoundPattern -> failwith "make_exact_entry" @@ -696,7 +696,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, let sigma' = Evd.merge_context_set univ_flexible sigma ctx in let ce = mk_clenv_from_env env sigma' None (c,cty) in let c' = clenv_type (* ~reduce:false *) ce in - let pat = pi3 (Patternops.pattern_of_constr env ce.evd c') in + let pat = Patternops.pattern_of_constr env ce.evd c' in let hd = try head_pattern_bound pat with BoundPattern -> failwith "make_apply_entry" in @@ -794,7 +794,7 @@ let make_trivial env sigma poly ?(name=PathAny) r = let ce = mk_clenv_from_env env sigma None (c,t) in (Some hd, { pri=1; poly = poly; - pat = Some (pi3 (Patternops.pattern_of_constr env ce.evd (clenv_type ce))); + pat = Some (Patternops.pattern_of_constr env ce.evd (clenv_type ce)); name = name; code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) }) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index d244129425..ee21a51598 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -688,12 +688,12 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = try Inl (coerce_to_evaluable_ref env x) with CannotCoerceTo _ -> let c = coerce_to_closed_constr env x in - Inr (pi3 (pattern_of_constr env sigma c)) in + Inr (pattern_of_constr env sigma c) in (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (loc,id) with Not_found -> error_global_not_found_loc loc (qualid_of_ident id)) | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b) - | Inr c -> Inr (pi3 (interp_typed_pattern ist env sigma c)) in + | Inr c -> Inr (interp_typed_pattern ist env sigma c) in interp_occurrences ist occs, p let interp_constr_with_occurrences_and_name_as_list = @@ -1043,7 +1043,7 @@ let use_types = false let eval_pattern lfun ist env sigma ((glob,_),pat as c) = let bound_names = bound_glob_vars glob in if use_types then - (bound_names,pi3 (interp_typed_pattern ist env sigma c)) + (bound_names,interp_typed_pattern ist env sigma c) else (bound_names,instantiate_pattern env sigma lfun pat) @@ -2154,7 +2154,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in Proofview.V82.tactic begin fun gl -> - let (sigma,sign,op) = interp_typed_pattern ist env sigma op in + let op = interp_typed_pattern ist env sigma op in let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in let c_interp patvars sigma = let lfun' = Id.Map.fold (fun id c lfun -> @@ -2167,7 +2167,7 @@ and interp_atomic ist tac : unit Proofview.tactic = errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.") in (Tactics.change (Some op) c_interp (interp_clause ist env sigma cl)) - { gl with sigma = sigma } + gl end end end |