From a91bafa58710777506dc30afb1a0e2cc56b941c7 Mon Sep 17 00:00:00 2001 From: thery Date: Tue, 5 Jul 2016 14:02:28 +0200 Subject: Bug fix : variable capture in ltac code of Nsatz changing set (x := val) into let x := fresh "x" in set (x := val) --- plugins/nsatz/Nsatz.v | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'plugins/nsatz') diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v index 3068b5347..b11d15e5c 100644 --- a/plugins/nsatz/Nsatz.v +++ b/plugins/nsatz/Nsatz.v @@ -298,7 +298,9 @@ Ltac nsatz_call_n info nparam p rr lp kont := match goal with | |- (?c::PEpow _ ?r::?lq0)::?lci0 = _ -> _ => intros _; + let lci := fresh "lci" in set (lci:=lci0); + let lq := fresh "lq" in set (lq:=lq0); kont c rr lq lci end. @@ -380,10 +382,13 @@ Ltac nsatz_generic radicalmax info lparam lvar := end in SplitPolyList ltac:(fun p lp => + let p21 := fresh "p21" in + let lp21 := fresh "lp21" in set (p21:=p) ; set (lp21:=lp); (* idtac "nparam:"; idtac nparam; idtac "p:"; idtac p; idtac "lp:"; idtac lp; *) nsatz_call radicalmax info nparam p lp ltac:(fun c r lq lci => + let q := fresh "q" in set (q := PEmul c (PEpow p21 r)); let Hg := fresh "Hg" in assert (Hg:check lp21 q (lci,lq) = true); -- cgit v1.2.3