diff options
Diffstat (limited to 'tactics/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 59791f011d..0e4091b3cb 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -268,12 +268,12 @@ let dummy_goal = {it = make_evar empty_named_context_val mkProp; sigma = empty} -let make_exact_entry pri (c,cty) = +let make_exact_entry sigma pri (c,cty) = let cty = strip_outer_cast cty in match kind_of_term cty with | Prod _ -> failwith "make_exact_entry" | _ -> - let pat = Pattern.pattern_of_constr cty in + let pat = Pattern.pattern_of_constr sigma cty in let head = try head_of_constr_reference (fst (head_constr cty)) with _ -> failwith "make_exact_entry" @@ -287,7 +287,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) = | Prod _ -> let ce = mk_clenv_from dummy_goal (c,cty) in let c' = clenv_type (* ~reduce:false *) ce in - let pat = Pattern.pattern_of_constr c' in + let pat = Pattern.pattern_of_constr sigma c' in let hd = (try head_pattern_bound pat with BoundPattern -> failwith "make_apply_entry") in let nmiss = List.length (clenv_missing ce) in @@ -317,7 +317,7 @@ let make_resolves env sigma flags pri c = let ents = map_succeed (fun f -> f (c,cty)) - [make_exact_entry pri; make_apply_entry env sigma flags pri] + [make_exact_entry sigma pri; make_apply_entry env sigma flags pri] in if ents = [] then errorlabstrm "Hint" @@ -354,7 +354,7 @@ let make_trivial env sigma c = let hd = head_of_constr_reference (fst (head_constr t)) in let ce = mk_clenv_from dummy_goal (c,t) in (Some hd, { pri=1; - pat = Some (Pattern.pattern_of_constr (clenv_type ce)); + pat = Some (Pattern.pattern_of_constr sigma (clenv_type ce)); code=Res_pf_THEN_trivial_fail(c,{ce with env=empty_env}) }) open Vernacexpr @@ -1102,7 +1102,7 @@ let make_resolve_any_hyp env sigma (id,_,ty) = let ents = map_succeed (fun f -> f (mkVar id,ty)) - [make_exact_entry None; make_apply_entry env sigma (true,true,false) None] + [make_exact_entry sigma None; make_apply_entry env sigma (true,true,false) None] in ents |