diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/merge.ml | 2 | ||||
| -rw-r--r-- | plugins/micromega/EnvRing.v | 2 | ||||
| -rw-r--r-- | plugins/rtauto/Bintree.v | 2 | ||||
| -rw-r--r-- | plugins/setoid_ring/InitialRing.v | 2 | ||||
| -rw-r--r-- | plugins/setoid_ring/Ring_polynom.v | 2 |
8 files changed, 8 insertions, 8 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index f69c4d8217..c424fe1226 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1432,7 +1432,7 @@ let do_build_inductive (* in *) let _time2 = System.get_time () in try - with_full_print (Flags.silently (Command.do_mutual_inductive true rel_inds (Flags.is_universe_polymorphism ()) false)) Decl_kinds.Finite + with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false)) Decl_kinds.Finite with | UserError(s,msg) as e -> let _time3 = System.get_time () in diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 8b3d3dc20f..0cacb003d8 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -400,7 +400,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp in evd,List.rev rev_pconstants | _ -> - Command.do_fixpoint ~flags:Declareops.safe_flags Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; + Command.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; let evd,rev_pconstants = List.fold_left (fun (evd,l) ((((_,fname),_),_,_,_,_),_) -> diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 94530bfde2..1ff254f6ca 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -365,7 +365,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes observe_tac("h_intro_patterns ") (let l = (List.nth intro_pats (pred i)) in match l with | [] -> tclIDTAC - | _ -> Proofview.V82.of_tactic (intro_patterns l)); + | _ -> Proofview.V82.of_tactic (intro_patterns false l)); (* unfolding of all the defined variables introduced by this branch *) (* observe_tac "unfolding" pre_tac; *) (* $zeta$ normalizing of the conclusion *) diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index a78eb1af76..99a165044c 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -887,7 +887,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive) let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in (* Declare inductive *) let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in - let mie,pl,impls = Command.interp_mutual_inductive true indl [] + let mie,pl,impls = Command.interp_mutual_inductive indl [] false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in (* Declare the mutual inductive block with its associated schemes *) ignore (Command.declare_mutual_inductive_with_eliminations mie pl impls) diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v index fd4bb248bf..904ee4dac1 100644 --- a/plugins/micromega/EnvRing.v +++ b/plugins/micromega/EnvRing.v @@ -914,7 +914,7 @@ Qed. revert P1. induction LM1 as [|(M2,P2') LM2 IH]; simpl; intros. - discriminate. - assert (H':=PNSubst_ok n P3 M2 P2'). destruct PNSubst. - * injection H; intros <-. rewrite <- PSubstL1_ok; intuition. + * injection H as <-. rewrite <- PSubstL1_ok; intuition. * now apply IH. Qed. diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v index 7394cebdef..3646018719 100644 --- a/plugins/rtauto/Bintree.v +++ b/plugins/rtauto/Bintree.v @@ -266,7 +266,7 @@ Qed. Lemma push_not_empty: forall a S, (push a S) <> empty. intros a [ind cont];unfold push,empty. -simpl;intro H;injection H; intros _ ; apply Pos.succ_not_1. +intros [= H%Pos.succ_not_1]. assumption. Qed. Fixpoint In (x:A) (S:Store) (F:Full S) {struct F}: Prop := diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index 8fcc077164..9c690e2b4a 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/plugins/setoid_ring/InitialRing.v @@ -96,7 +96,7 @@ Section ZMORPHISM. Proof. constructor. destruct c;intros;try discriminate. - injection H;clear H;intros H1;subst c'. + injection H as <-. simpl. unfold Zeq_bool. rewrite Z.compare_refl. trivial. Qed. diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index 760ad4da11..b69196679f 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -883,7 +883,7 @@ Section MakeRingPol. revert P1. induction LM1 as [|(M2,P2') LM2 IH]; simpl; intros. - discriminate. - assert (H':=PNSubst_ok n P3 M2 P2'). destruct PNSubst. - * injection H; intros <-. rewrite <- PSubstL1_ok; intuition. + * injection H as <-. rewrite <- PSubstL1_ok; intuition. * now apply IH. Qed. |