From 4be2dd481c783bed7c09086b647d860e42b7ea9f Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Fri, 7 Sep 2018 11:18:28 +0200 Subject: Retroknowledge.KInt31: remove the (unused) group parameter --- theories/Numbers/Cyclic/Int31/Int31.v | 38 +++++++++++++++++------------------ 1 file changed, 19 insertions(+), 19 deletions(-) (limited to 'theories/Numbers') diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index 77ab624ca5..5c1c5d794d 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -45,8 +45,8 @@ Inductive int31 : Type := I31 : digits31 int31. (* spiwack: Registration of the type of integers, so that the matchs in the functions below perform dynamic decompilation (otherwise some segfault occur when they are applied to one non-closed term and one closed term). *) -Register digits as int31 bits in "coq_int31" by True. -Register int31 as int31 type in "coq_int31" by True. +Register digits as int31 bits by True. +Register int31 as int31 type by True. Declare Scope int31_scope. Declare ML Module "int31_syntax_plugin". @@ -345,21 +345,21 @@ Definition lor31 n m := phi_inv (Z.lor (phi n) (phi m)). Definition land31 n m := phi_inv (Z.land (phi n) (phi m)). Definition lxor31 n m := phi_inv (Z.lxor (phi n) (phi m)). -Register add31 as int31 plus in "coq_int31" by True. -Register add31c as int31 plusc in "coq_int31" by True. -Register add31carryc as int31 pluscarryc in "coq_int31" by True. -Register sub31 as int31 minus in "coq_int31" by True. -Register sub31c as int31 minusc in "coq_int31" by True. -Register sub31carryc as int31 minuscarryc in "coq_int31" by True. -Register mul31 as int31 times in "coq_int31" by True. -Register mul31c as int31 timesc in "coq_int31" by True. -Register div3121 as int31 div21 in "coq_int31" by True. -Register div31 as int31 diveucl in "coq_int31" by True. -Register compare31 as int31 compare in "coq_int31" by True. -Register addmuldiv31 as int31 addmuldiv in "coq_int31" by True. -Register lor31 as int31 lor in "coq_int31" by True. -Register land31 as int31 land in "coq_int31" by True. -Register lxor31 as int31 lxor in "coq_int31" by True. +Register add31 as int31 plus by True. +Register add31c as int31 plusc by True. +Register add31carryc as int31 pluscarryc by True. +Register sub31 as int31 minus by True. +Register sub31c as int31 minusc by True. +Register sub31carryc as int31 minuscarryc by True. +Register mul31 as int31 times by True. +Register mul31c as int31 timesc by True. +Register div3121 as int31 div21 by True. +Register div31 as int31 diveucl by True. +Register compare31 as int31 compare by True. +Register addmuldiv31 as int31 addmuldiv by True. +Register lor31 as int31 lor by True. +Register land31 as int31 land by True. +Register lxor31 as int31 lxor by True. Definition lnot31 n := lxor31 Tn n. Definition ldiff31 n m := land31 n (lnot31 m). @@ -485,5 +485,5 @@ Definition tail031 (i:int31) := end) i On. -Register head031 as int31 head0 in "coq_int31" by True. -Register tail031 as int31 tail0 in "coq_int31" by True. +Register head031 as int31 head0 by True. +Register tail031 as int31 tail0 by True. -- cgit v1.2.3 From ab2560233f2e6fc8c26853af6991533d8d335e16 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Fri, 7 Sep 2018 11:34:32 +0200 Subject: Retroknowledge: remove the (unused) by clause --- theories/Numbers/Cyclic/Int31/Int31.v | 38 +++++++++++++++++------------------ 1 file changed, 19 insertions(+), 19 deletions(-) (limited to 'theories/Numbers') diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index 5c1c5d794d..f1b02759c5 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -45,8 +45,8 @@ Inductive int31 : Type := I31 : digits31 int31. (* spiwack: Registration of the type of integers, so that the matchs in the functions below perform dynamic decompilation (otherwise some segfault occur when they are applied to one non-closed term and one closed term). *) -Register digits as int31 bits by True. -Register int31 as int31 type by True. +Register digits as int31 bits. +Register int31 as int31 type. Declare Scope int31_scope. Declare ML Module "int31_syntax_plugin". @@ -345,21 +345,21 @@ Definition lor31 n m := phi_inv (Z.lor (phi n) (phi m)). Definition land31 n m := phi_inv (Z.land (phi n) (phi m)). Definition lxor31 n m := phi_inv (Z.lxor (phi n) (phi m)). -Register add31 as int31 plus by True. -Register add31c as int31 plusc by True. -Register add31carryc as int31 pluscarryc by True. -Register sub31 as int31 minus by True. -Register sub31c as int31 minusc by True. -Register sub31carryc as int31 minuscarryc by True. -Register mul31 as int31 times by True. -Register mul31c as int31 timesc by True. -Register div3121 as int31 div21 by True. -Register div31 as int31 diveucl by True. -Register compare31 as int31 compare by True. -Register addmuldiv31 as int31 addmuldiv by True. -Register lor31 as int31 lor by True. -Register land31 as int31 land by True. -Register lxor31 as int31 lxor by True. +Register add31 as int31 plus. +Register add31c as int31 plusc. +Register add31carryc as int31 pluscarryc. +Register sub31 as int31 minus. +Register sub31c as int31 minusc. +Register sub31carryc as int31 minuscarryc. +Register mul31 as int31 times. +Register mul31c as int31 timesc. +Register div3121 as int31 div21. +Register div31 as int31 diveucl. +Register compare31 as int31 compare. +Register addmuldiv31 as int31 addmuldiv. +Register lor31 as int31 lor. +Register land31 as int31 land. +Register lxor31 as int31 lxor. Definition lnot31 n := lxor31 Tn n. Definition ldiff31 n m := land31 n (lnot31 m). @@ -485,5 +485,5 @@ Definition tail031 (i:int31) := end) i On. -Register head031 as int31 head0 by True. -Register tail031 as int31 tail0 by True. +Register head031 as int31 head0. +Register tail031 as int31 tail0. -- cgit v1.2.3 From 736842d4cde09c667837dee8a633ff98ecf6a820 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Mon, 10 Sep 2018 13:20:39 +0200 Subject: Register: simpler syntax --- theories/Numbers/Cyclic/Int31/Int31.v | 38 +++++++++++++++++------------------ 1 file changed, 19 insertions(+), 19 deletions(-) (limited to 'theories/Numbers') diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index f1b02759c5..ca7d3ec074 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -45,8 +45,8 @@ Inductive int31 : Type := I31 : digits31 int31. (* spiwack: Registration of the type of integers, so that the matchs in the functions below perform dynamic decompilation (otherwise some segfault occur when they are applied to one non-closed term and one closed term). *) -Register digits as int31 bits. -Register int31 as int31 type. +Register digits as int31.bits. +Register int31 as int31.type. Declare Scope int31_scope. Declare ML Module "int31_syntax_plugin". @@ -345,21 +345,21 @@ Definition lor31 n m := phi_inv (Z.lor (phi n) (phi m)). Definition land31 n m := phi_inv (Z.land (phi n) (phi m)). Definition lxor31 n m := phi_inv (Z.lxor (phi n) (phi m)). -Register add31 as int31 plus. -Register add31c as int31 plusc. -Register add31carryc as int31 pluscarryc. -Register sub31 as int31 minus. -Register sub31c as int31 minusc. -Register sub31carryc as int31 minuscarryc. -Register mul31 as int31 times. -Register mul31c as int31 timesc. -Register div3121 as int31 div21. -Register div31 as int31 diveucl. -Register compare31 as int31 compare. -Register addmuldiv31 as int31 addmuldiv. -Register lor31 as int31 lor. -Register land31 as int31 land. -Register lxor31 as int31 lxor. +Register add31 as int31.plus. +Register add31c as int31.plusc. +Register add31carryc as int31.pluscarryc. +Register sub31 as int31.minus. +Register sub31c as int31.minusc. +Register sub31carryc as int31.minuscarryc. +Register mul31 as int31.times. +Register mul31c as int31.timesc. +Register div3121 as int31.div21. +Register div31 as int31.diveucl. +Register compare31 as int31.compare. +Register addmuldiv31 as int31.addmuldiv. +Register lor31 as int31.lor. +Register land31 as int31.land. +Register lxor31 as int31.lxor. Definition lnot31 n := lxor31 Tn n. Definition ldiff31 n m := land31 n (lnot31 m). @@ -485,5 +485,5 @@ Definition tail031 (i:int31) := end) i On. -Register head031 as int31 head0. -Register tail031 as int31 tail0. +Register head031 as int31.head0. +Register tail031 as int31.tail0. -- cgit v1.2.3