diff options
| author | Matthieu Sozeau | 2014-09-27 16:34:24 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-27 20:41:04 +0200 |
| commit | 0f17c70288662bf8abd1bae59d32a94054481f26 (patch) | |
| tree | f604cd6de5f1274b3e54dcfe48bc84cf0494d473 /tactics | |
| parent | 84544396cbbf34848be2240acf181b4d5f1f42d2 (diff) | |
Make pattern_of_constr typed so that we can infer the proper patterns
for primitive projections, fixing bug #3661. Also fix expand_projection
so that it does enough reduction to find the inductive type of its
argument.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 564e111e04..356b208b8e 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -604,7 +604,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, let sigma' = Evd.merge_context_set univ_flexible dummy_goal.sigma ctx in let ce = mk_clenv_from { dummy_goal with sigma = sigma' } (c,cty) in let c' = clenv_type (* ~reduce:false *) ce in - let pat = snd (Patternops.pattern_of_constr env sigma c') in + let pat = snd (Patternops.pattern_of_constr env ce.evd c') in let hd = try head_pattern_bound pat with BoundPattern -> failwith "make_apply_entry" in @@ -701,7 +701,7 @@ let make_trivial env sigma poly ?(name=PathAny) r = let ce = mk_clenv_from dummy_goal (c,t) in (Some hd, { pri=1; poly = poly; - pat = Some (snd (Patternops.pattern_of_constr env sigma (clenv_type ce))); + pat = Some (snd (Patternops.pattern_of_constr env ce.evd (clenv_type ce))); name = name; code=Res_pf_THEN_trivial_fail(c,t,ctx) }) |