Bug fix : variable capture in ltac code of Nsatz

changing
set (x := val)
into
let x := fresh "x" in
set (x := val)

1 files changed, 5 insertions, 0 deletions

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);