diff options
| author | Pierre-Marie Pédrot | 2015-03-04 16:22:24 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-03-04 16:22:24 +0100 |
| commit | a348471ec6303b9b080d77cf0ca7a58c21aa6369 (patch) | |
| tree | 0746249e326b92fb21f98fe71e467f0ee0215058 /tactics | |
| parent | d169ecbac96fe2a8a6a44395ad7fa83612e725c4 (diff) | |
| parent | 00018101cf81f69d23587985a16fe3c8eefb8eaf (diff) | |
Merge branch 'v8.5'
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 5621c365aa..101223b570 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -609,7 +609,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 = snd (Patternops.pattern_of_constr env sigma cty) in + let pat = pi3 (Patternops.pattern_of_constr env sigma cty) in let hd = try head_pattern_bound pat with BoundPattern -> failwith "make_exact_entry" @@ -628,7 +628,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 = snd (Patternops.pattern_of_constr env ce.evd c') in + let pat = pi3 (Patternops.pattern_of_constr env ce.evd c') in let hd = try head_pattern_bound pat with BoundPattern -> failwith "make_apply_entry" in @@ -726,7 +726,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 (snd (Patternops.pattern_of_constr env ce.evd (clenv_type ce))); + pat = Some (pi3 (Patternops.pattern_of_constr env ce.evd (clenv_type ce))); name = name; code=Res_pf_THEN_trivial_fail(c,t,ctx) }) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 8826875a38..1429211f19 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -681,7 +681,7 @@ let interp_constr_with_occurrences ist env sigma (occs,c) = let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = let p = match a with | Inl b -> Inl (interp_evaluable ist env sigma b) - | Inr c -> Inr (snd (interp_typed_pattern ist env sigma c)) in + | Inr c -> Inr (pi3 (interp_typed_pattern ist env sigma c)) in interp_occurrences ist occs, p let interp_constr_with_occurrences_and_name_as_list = @@ -1030,7 +1030,7 @@ let use_types = false let eval_pattern lfun ist env sigma (_,pat as c) = if use_types then - snd (interp_typed_pattern ist env sigma c) + pi3 (interp_typed_pattern ist env sigma c) else instantiate_pattern env sigma lfun pat @@ -2138,7 +2138,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 sign,op = interp_typed_pattern ist env sigma op in + let (sigma,sign,op) = interp_typed_pattern ist env sigma op in let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in let env' = Environ.push_named_context sign env in let c_interp sigma = @@ -2146,8 +2146,8 @@ and interp_atomic ist tac : unit Proofview.tactic = with e when to_catch e (* Hack *) -> 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 + (Tactics.change (Some op) c_interp (interp_clause ist env sigma cl)) + { gl with sigma = sigma } end end end |