diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-07-07 20:27:56 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-07-07 20:31:30 +0200 |
| commit | 17d8a49247ad82ca59def4c577031101f61bbf08 (patch) | |
| tree | 8ee004df8d6ff7e252f346e3593169e374de8796 /plugins/nsatz | |
| parent | 21be7a5dba2fdfa40fd7b4a3d94610947d202bb7 (diff) | |
| parent | 947b30150602ba951efa4717d30d4a380482a963 (diff) | |
Merge branch 'v8.5' into v8.6
Diffstat (limited to 'plugins/nsatz')
| -rw-r--r-- | plugins/nsatz/Nsatz.v | 5 |
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); |