From d2c5c5e616a6e118291fe1ce9965c731adac03a8 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 19 Jan 2014 15:09:23 +0100 Subject: Imported Upstream version 8.4pl3dfsg --- plugins/nsatz/Nsatz.v | 4 ++-- plugins/setoid_ring/Field_tac.v | 6 ++++-- plugins/setoid_ring/Field_theory.v | 16 +++++++++------- plugins/subtac/subtac_obligations.ml | 10 +++++++--- plugins/xml/cic2acic.ml | 2 +- plugins/xml/xmlcommand.ml | 26 +++++++++++++------------- 6 files changed, 36 insertions(+), 28 deletions(-) (limited to 'plugins') diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v index 4f4f2039..7b746396 100644 --- a/plugins/nsatz/Nsatz.v +++ b/plugins/nsatz/Nsatz.v @@ -248,11 +248,11 @@ Fixpoint interpret3 t fv {struct t}: R := End nsatz1. Ltac equality_to_goal H x y:= - let h := fresh "nH" in (* eliminate trivial hypotheses, but it takes time!: + let h := fresh "nH" in (assert (h:equality x y); [solve [cring] | clear H; clear h]) - || *) (try generalize (@psos_r1 _ _ _ _ _ _ _ _ _ _ _ x y H); clear H) + || *) try (generalize (@psos_r1 _ _ _ _ _ _ _ _ _ _ _ x y H); clear H) . Ltac equalities_to_goal := diff --git a/plugins/setoid_ring/Field_tac.v b/plugins/setoid_ring/Field_tac.v index 8ac952c0..013fd0ef 100644 --- a/plugins/setoid_ring/Field_tac.v +++ b/plugins/setoid_ring/Field_tac.v @@ -201,7 +201,8 @@ Ltac fold_field_cond req := Ltac simpl_PCond FLD := let req := get_FldEq FLD in let lemma := get_CondLemma FLD in - try apply lemma; + try (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; + clear lock_def lock); protect_fv "field_cond"; fold_field_cond req; try exact I. @@ -209,7 +210,8 @@ Ltac simpl_PCond FLD := Ltac simpl_PCond_BEURK FLD := let req := get_FldEq FLD in let lemma := get_CondLemma FLD in - apply lemma; + try (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; + clear lock_def lock); protect_fv "field_cond"; fold_field_cond req. diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index bc05c252..1989e9b3 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -1507,13 +1507,15 @@ Fixpoint Fapp (l m:list (PExpr C)) {struct l} : list (PExpr C) := | cons a l1 => Fcons a (Fapp l1 m) end. -Lemma fcons_correct : forall l l1, - PCond l (Fapp l1 nil) -> PCond l l1. -induction l1; simpl; intros. - trivial. - elim PCond_fcons_inv with (1 := H); intros. - destruct l1; auto. -Qed. + Lemma fcons_correct : forall l l1, + (forall lock, lock = PCond l -> lock (Fapp l1 nil)) -> PCond l l1. + Proof. + intros l l1 h1; assert (H := h1 (PCond l) (refl_equal _));clear h1. + induction l1; simpl; intros. + trivial. + elim PCond_fcons_inv with (1 := H); intros. + destruct l1; trivial. split; trivial. apply IHl1; trivial. + Qed. End Fcons_impl. diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index d8f46098..7a4916fa 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -559,14 +559,18 @@ and solve_prg_obligations prg ?oblset tac = let obls, rem = prg.prg_obligations in let rem = ref rem in let obls' = Array.copy obls in + let set = ref Intset.empty in let p = match oblset with | None -> (fun _ -> true) - | Some s -> (fun i -> Intset.mem i s) + | Some s -> set := s; + (fun i -> Intset.mem i !set) in let _ = Array.iteri (fun i x -> - if p i && solve_obligation_by_tac prg obls' i tac then - decr rem) + if p i && solve_obligation_by_tac prg obls' i tac then + let deps = dependencies obls i in + (set := Intset.union !set deps; + decr rem)) obls' in update_obls prg obls' !rem diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index a14eda60..165bf83d 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -23,7 +23,7 @@ let get_module_path_of_full_path path = (function modul -> Libnames.is_dirpath_prefix_of modul dirpath) modules with [] -> - Pp.warning ("Modules not supported: reference to "^ + Pp.msg_warn ("Modules not supported: reference to "^ Libnames.string_of_path path^" will be wrong"); dirpath | [modul] -> modul diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 867aac71..59ade01e 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -433,46 +433,46 @@ let kind_of_constant kn = | DK.IsAssumption DK.Definitional -> "AXIOM","Declaration" | DK.IsAssumption DK.Logical -> "AXIOM","Axiom" | DK.IsAssumption DK.Conjectural -> - Pp.warning "Conjecture not supported in dtd (used Declaration instead)"; + Pp.msg_warn "Conjecture not supported in dtd (used Declaration instead)"; "AXIOM","Declaration" | DK.IsDefinition DK.Definition -> "DEFINITION","Definition" | DK.IsDefinition DK.Example -> - Pp.warning "Example not supported in dtd (used Definition instead)"; + Pp.msg_warn "Example not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.Coercion -> - Pp.warning "Coercion not supported in dtd (used Definition instead)"; + Pp.msg_warn "Coercion not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.SubClass -> - Pp.warning "SubClass not supported in dtd (used Definition instead)"; + Pp.msg_warn "SubClass not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.CanonicalStructure -> - Pp.warning "CanonicalStructure not supported in dtd (used Definition instead)"; + Pp.msg_warn "CanonicalStructure not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.Fixpoint -> - Pp.warning "Fixpoint not supported in dtd (used Definition instead)"; + Pp.msg_warn "Fixpoint not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.CoFixpoint -> - Pp.warning "CoFixpoint not supported in dtd (used Definition instead)"; + Pp.msg_warn "CoFixpoint not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.Scheme -> - Pp.warning "Scheme not supported in dtd (used Definition instead)"; + Pp.msg_warn "Scheme not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.StructureComponent -> - Pp.warning "StructureComponent not supported in dtd (used Definition instead)"; + Pp.msg_warn "StructureComponent not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.IdentityCoercion -> - Pp.warning "IdentityCoercion not supported in dtd (used Definition instead)"; + Pp.msg_warn "IdentityCoercion not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.Instance -> - Pp.warning "Instance not supported in dtd (used Definition instead)"; + Pp.msg_warn "Instance not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.Method -> - Pp.warning "Method not supported in dtd (used Definition instead)"; + Pp.msg_warn "Method not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsProof (DK.Theorem|DK.Lemma|DK.Corollary|DK.Fact|DK.Remark as thm) -> "THEOREM",DK.string_of_theorem_kind thm | DK.IsProof _ -> - Pp.warning "Unsupported theorem kind (used Theorem instead)"; + Pp.msg_warn "Unsupported theorem kind (used Theorem instead)"; "THEOREM",DK.string_of_theorem_kind DK.Theorem ;; -- cgit v1.2.3