diff options
| -rw-r--r-- | tactics/auto.ml | 17 | ||||
| -rw-r--r-- | tactics/class_tactics.ml4 | 22 | ||||
| -rw-r--r-- | theories/Sets/Integers.v | 1 |
3 files changed, 30 insertions, 10 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index b6dc4e598..6a08bda87 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -270,13 +270,16 @@ let dummy_goal = let make_exact_entry pri (c,cty) = let cty = strip_outer_cast cty in - let pat = Pattern.pattern_of_constr cty in - let head = - try head_of_constr_reference (fst (head_constr cty)) - with _ -> failwith "make_exact_entry" - in - (Some head, - { pri=(match pri with Some pri -> pri | None -> 0); pat=Some pat; code=Give_exact c }) + match kind_of_term cty with + | Prod _ -> failwith "make_exact_entry" + | _ -> + let pat = Pattern.pattern_of_constr cty in + let head = + try head_of_constr_reference (fst (head_constr cty)) + with _ -> failwith "make_exact_entry" + in + (Some head, + { pri=(match pri with Some pri -> pri | None -> 0); pat=Some pat; code=Give_exact c }) let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) = let cty = if hnf then hnf_constr env sigma cty else cty in diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 23d92429e..6f928e096 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -139,6 +139,20 @@ let unify_resolve flags (c,clenv) gls = let clenv' = clenv_unique_resolver false ~flags clenv' gls in tclPROGRESS (Clenvtac.clenv_refine false ~with_classes:false clenv') gls +let clenv_of_prods nprods (c, clenv) gls = + if nprods = 0 then Some clenv + else + let ty = pf_type_of gls c in + let diff = nb_prod ty - nprods in + if diff >= 0 then + Some (mk_clenv_from_n gls (Some diff) (c,ty)) + else None + +let with_prods nprods (c, clenv) f gls = + match clenv_of_prods nprods (c, clenv) gls with + | None -> tclFAIL 0 (str"Not enough premisses") gls + | Some clenv' -> f (c, clenv') gls + (** Hack to properly solve dependent evars that are typeclasses *) let flags_of_state st = @@ -160,6 +174,8 @@ let rec e_trivial_fail_db db_list local_db goal = and e_my_find_search db_list local_db hdc concl = let hdc = head_of_constr_reference hdc in + let prods, concl = decompose_prod_assum concl in + let nprods = List.length prods in let hintl = list_map_append (fun db -> @@ -175,11 +191,11 @@ and e_my_find_search db_list local_db hdc concl = fun (flags, {pri=b; pat = p; code=t}) -> let tac = match t with - | Res_pf (term,cl) -> unify_resolve flags (term,cl) - | ERes_pf (term,cl) -> unify_e_resolve flags (term,cl) + | Res_pf (term,cl) -> with_prods nprods (term,cl) (unify_resolve flags) + | ERes_pf (term,cl) -> with_prods nprods (term,cl) (unify_e_resolve flags) | Give_exact (c) -> e_give_exact flags c | Res_pf_THEN_trivial_fail (term,cl) -> - tclTHEN (unify_e_resolve flags (term,cl)) + tclTHEN (with_prods nprods (term,cl) (unify_e_resolve flags)) (e_trivial_fail_db db_list local_db) | Unfold_nth c -> tclWEAK_PROGRESS (unfold_in_concl [all_occurrences,c]) | Extern tacast -> conclPattern concl p tacast diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v index 01d3bda37..15c1b665e 100644 --- a/theories/Sets/Integers.v +++ b/theories/Sets/Integers.v @@ -79,6 +79,7 @@ Section Integers_sect. auto with sets arith. apply Inhabited_intro with (x := 0). apply Integers_defn. + exact le_Order. Defined. Lemma le_total_order : Totally_ordered nat nat_po Integers. |