From 33d54f6692446e6006f9b89d0dfd64408a4051fe Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 17 Nov 2011 22:19:36 +0000 Subject: Fixing bug #2640 and variants of it (inconsistency between when and how the names of an ltac expression are globalized - allowing the expression to be a constr and in some initial context - and when and how this ltac expression is interpreted - now expecting a pure tactic in a different context). This incidentally found a Ltac bug in Ncring_polynom! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14676 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/decl_mode/decl_interp.ml | 2 +- plugins/setoid_ring/Ncring_polynom.v | 6 +++--- plugins/setoid_ring/newring.ml4 | 16 ++++++++-------- plugins/subtac/subtac_utils.ml | 2 +- plugins/xml/dumptree.ml4 | 2 +- plugins/xml/proofTree2Xml.ml4 | 2 +- 6 files changed, 15 insertions(+), 15 deletions(-) (limited to 'plugins') diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 64aa08ff2..b3e076c49 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -27,7 +27,7 @@ let intern_justification_items globs = Option.map (List.map (intern_constr globs)) let intern_justification_method globs = - Option.map (intern_tactic globs) + Option.map (intern_pure_tactic globs) let intern_statement intern_it globs st = {st_label=st.st_label; diff --git a/plugins/setoid_ring/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v index a3e14b30f..c0d315871 100644 --- a/plugins/setoid_ring/Ncring_polynom.v +++ b/plugins/setoid_ring/Ncring_polynom.v @@ -23,7 +23,7 @@ Context (C R:Type) `{Rh:Ring_morphism C R}. Variable phiCR_comm: forall (c:C)(x:R), x * [c] == [c] * x. - Ltac rsimpl := repeat (gen_rewrite || phiCR_comm). + Ltac rsimpl := repeat (gen_rewrite || rewrite phiCR_comm). Ltac add_push := gen_add_push . (* Definition of non commutative multivariable polynomials @@ -298,7 +298,7 @@ reflexivity. induction P;simpl;intros. rewrite ring_morphism_mul. try reflexivity. simpl. Esimpl. rewrite IHP1;rewrite IHP2;rsimpl. - repeat rewrite phiCR_comm. Esimpl. Qed. + Qed. Lemma PmulC_ok : forall c P l, (PmulC P c)@l == P@l * [c]. Proof. @@ -618,4 +618,4 @@ exact pow_th. apply Peq_ok;trivial. Qed. -End MakeRingPol. \ No newline at end of file +End MakeRingPol. diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index af236bc0f..d189a4e55 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -164,11 +164,11 @@ let decl_constant na c = (* Calling a global tactic *) let ltac_call tac (args:glob_tactic_arg list) = - TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args)) + TacArg(dummy_loc,TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args)) (* Calling a locally bound tactic *) let ltac_lcall tac args = - TacArg(TacCall(dummy_loc, ArgVar(dummy_loc, id_of_string tac),args)) + TacArg(dummy_loc,TacCall(dummy_loc, ArgVar(dummy_loc, id_of_string tac),args)) let ltac_letin (x, e1) e2 = TacLetIn(false,[(dummy_loc,id_of_string x),e1],e2) @@ -624,23 +624,23 @@ let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac = (match rk, opp, kind with Abstract, None, _ -> let t = ArgArg(dummy_loc,Lazy.force ltac_inv_morphN) in - TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul])) + TacArg(dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul])) | Abstract, Some opp, Some _ -> let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphZ) in - TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp])) + TacArg(dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp])) | Abstract, Some opp, None -> let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphNword) in TacArg - (TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp])) + (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp])) | Computational _,_,_ -> let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in TacArg - (TacCall(dummy_loc,t,List.map carg [zero;one;zero;one])) + (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;zero;one])) | Morphism mth,_,_ -> let (_,czero,cone,_,_,_,_,_,_) = dest_morph env sigma mth in let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in TacArg - (TacCall(dummy_loc,t,List.map carg [zero;one;czero;cone]))) + (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;czero;cone]))) let make_hyp env c = let t = Retyping.get_type_of env Evd.empty c in @@ -657,7 +657,7 @@ let interp_power env pow = match pow with | None -> let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_nothing) in - (TacArg(TacCall(dummy_loc,t,[])), lapp coq_None [|carrier|]) + (TacArg(dummy_loc,TacCall(dummy_loc,t,[])), lapp coq_None [|carrier|]) | Some (tac, spec) -> let tac = match tac with diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml index ae28c9847..546d720c4 100644 --- a/plugins/subtac/subtac_utils.ml +++ b/plugins/subtac/subtac_utils.ml @@ -474,4 +474,4 @@ let tactics_tac s = lazy(make_kn (MPfile contrib_tactics_path) (make_dirpath []) (mk_label s)) let tactics_call tac args = - TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (tactics_tac tac)),args)) + TacArg(dummy_loc,TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (tactics_tac tac)),args)) diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4 index 44a481f44..3c3e54fa3 100644 --- a/plugins/xml/dumptree.ml4 +++ b/plugins/xml/dumptree.ml4 @@ -42,7 +42,7 @@ let thin_sign osign sign = ;; let pr_tactic_xml = function - | TacArg (Tacexp t) -> str "" + | TacArg (_,Tacexp t) -> str "" | t -> str "" ;; diff --git a/plugins/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4 index b0e4fcc69..2f5eb6ac2 100644 --- a/plugins/xml/proofTree2Xml.ml4 +++ b/plugins/xml/proofTree2Xml.ml4 @@ -144,7 +144,7 @@ Pp.ppnl (Pp.(++) (Pp.str Proof2aproof.ProofTreeHash.find proof_tree_to_flattened_proof_tree node in begin match tactic_expr with - | T.TacArg (T.Tacexp _) -> + | T.TacArg (_,T.Tacexp _) -> (* We don't need to keep the level of abstraction introduced at *) (* user-level invocation of tactic... (see Tacinterp.hide_interp)*) aux flat_proof old_hyps -- cgit v1.2.3