diff options
-rw-r--r-- | plugins/rtauto/Bintree.v | 8 | ||||
-rw-r--r-- | plugins/rtauto/Rtauto.v | 2 | ||||
-rw-r--r-- | pretyping/pretyping.ml | 1 | ||||
-rw-r--r-- | proofs/clenv.ml | 1 | ||||
-rw-r--r-- | theories/Sets/Finite_sets_facts.v | 4 |
5 files changed, 9 insertions, 7 deletions
diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v index d68fb1656..769869584 100644 --- a/plugins/rtauto/Bintree.v +++ b/plugins/rtauto/Bintree.v @@ -87,7 +87,7 @@ end. Theorem pos_eq_refl : forall m n, pos_eq m n = true -> m = n. induction m;simpl;intro n;destruct n;congruence || -(intro e;apply f_equal with positive;auto). +(intro e;apply f_equal;auto). Defined. Theorem refl_pos_eq : forall m, pos_eq m m = true. @@ -140,7 +140,7 @@ end. Theorem nat_eq_refl : forall m n, nat_eq m n = true -> m = n. induction m;simpl;intro n;destruct n;congruence || -(intro e;apply f_equal with nat;auto). +(intro e;apply f_equal;auto). Defined. Theorem refl_nat_eq : forall n, nat_eq n n = true. @@ -161,14 +161,14 @@ List.map f (l ++ m) = List.map f l ++ List.map f m. induction l. reflexivity. simpl. -intro m ; apply f_equal with (list B);apply IHl. +intro m ; apply f_equal;apply IHl. Qed. Lemma length_map : forall (A B:Set) (f:A -> B) l, length (List.map f l) = length l. induction l. reflexivity. -simpl; apply f_equal with nat;apply IHl. +simpl; apply f_equal;apply IHl. Qed. Lemma Lget_map : forall (A B:Set) (f:A -> B) i l, diff --git a/plugins/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v index 63e6717a0..e80542831 100644 --- a/plugins/rtauto/Rtauto.v +++ b/plugins/rtauto/Rtauto.v @@ -41,7 +41,7 @@ end. Theorem pos_eq_refl : forall m n, pos_eq m n = true -> m = n. induction m;simpl;destruct n;congruence || -(intro e;apply f_equal with positive;auto). +(intro e;apply f_equal;auto). Qed. Fixpoint form_eq (p q:form) {struct p} :bool := diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index dfd92f0c1..8898e5989 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -717,6 +717,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let understand_judgment_tcc evdref env c = let j = pretype empty_tycon env evdref ([],[]) c in + evdref := Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true ~fail:false env !evdref; j_nf_evar !evdref j (* Raw calls to the unsafe inference machine: boolean says if we must diff --git a/proofs/clenv.ml b/proofs/clenv.ml index ca77e10c8..a8b13e845 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -229,6 +229,7 @@ let clenv_dependent hyps_only clenv = let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in let deps = dependent_metas clenv mvs ctyp_mvs in let nonlinear = duplicated_metas (clenv_value clenv) in + let ctyp_mvs = dependent_metas clenv (Metaset.elements ctyp_mvs) ctyp_mvs in (* Make the assumption that duplicated metas have internal dependencies *) List.filter (fun mv -> if Metaset.mem mv deps diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v index ec0f0361d..350cd783c 100644 --- a/theories/Sets/Finite_sets_facts.v +++ b/theories/Sets/Finite_sets_facts.v @@ -173,14 +173,14 @@ Section Finite_sets_facts. clear H'2 c2 Y. intros X0 c2 H'2 H'3 x0 H'4 H'5. elim (classic (In U X0 x)). - intro H'6; apply f_equal with nat. + intro H'6; apply f_equal. apply H'0 with (Y := Subtract U (Add U X0 x0) x). elimtype (pred (S c2) = c2); auto with sets. apply card_soustr_1; auto with sets. rewrite <- H'5. apply Sub_Add_new; auto with sets. elim (classic (x = x0)). - intros H'6 H'7; apply f_equal with nat. + intros H'6 H'7; apply f_equal. apply H'0 with (Y := X0); auto with sets. apply Simplify_add with (x := x); auto with sets. pattern x at 2 in |- *; rewrite H'6; auto with sets. |