Workaround an issue in jsCoq

math-comp · Dec 8, 2022 · fc1ebd5 · fc1ebd5
1 parent 4d43302
commit fc1ebd5
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 11 deletions.
diff --git a/theories/common.elpi b/theories/common.elpi
@@ -77,13 +77,13 @@ ground-uint {{ Number.UIntDecimal lp:D }} :- !, ground-decimal D.
 ground-uint {{ Number.UIntHexadecimal lp:D }} :- !, ground-hexadecimal D.
 
 pred reduction-pos i:term, o:term.
-reduction-pos I O :- coq.reduction.vm.norm I {{ positive }} O, ground-pos O.
+reduction-pos I O :- coq.reduction.cbv.norm I O, ground-pos O.
 
 pred reduction-N i:term, o:term.
-reduction-N I O :- coq.reduction.vm.norm I {{ N }} O, ground-N O.
+reduction-N I O :- coq.reduction.cbv.norm I O, ground-N O.
 
 pred reduction-Z i:term, o:term.
-reduction-Z I O :- coq.reduction.vm.norm I {{ Z }} O, ground-Z O.
+reduction-Z I O :- coq.reduction.cbv.norm I O, ground-Z O.
 
 pred negb i:bool, o:bool.
 negb tt ff :- !.

diff --git a/theories/lra.elpi b/theories/lra.elpi
@@ -141,7 +141,7 @@ coqZ->Q tt (coqZneg P) {{ Qmake (-1) lp:P }} :- !.
 pred quote.nat i:term, o:term, o:coqZ.
 quote.nat {{ Nat.of_num_uint lp:X }} {{ large_nat_uint lp:X }} Out :-
   ground-uint X, !,
-  coq.reduction.vm.norm {{ N.of_num_uint lp:X }} {{ N }} XN, !,
+  coq.reduction.cbv.norm {{ N.of_num_uint lp:X }} XN, !,
   coqZ->N Out XN.
 quote.nat X {{ large_nat_N lp:XN }} Out :-
   reduction-N {{ N.of_nat lp:X }} XN, !, coqZ->N Out XN.
@@ -151,13 +151,13 @@ quote.nat X {{ large_nat_N lp:XN }} Out :-
 pred quote.int i:term, o:term, o:coqZ.
 quote.int {{ Posz (Nat.of_num_uint lp:X) }} {{ large_int_Pos lp:X }} Out :-
   ground-uint X, !,
-  coq.reduction.vm.norm {{ N.of_num_uint lp:X }} {{ N }} XN, !, coqZ->N Out XN.
+  coq.reduction.cbv.norm {{ N.of_num_uint lp:X }} XN, !, coqZ->N Out XN.
 quote.int {{ Posz lp:N }} {{ large_int_Z lp:NZ }} Out :-
   reduction-Z {{ Z.of_nat lp:N }} NZ, !, coqZ->Z Out NZ.
 quote.int {{ Negz (Nat.of_num_uint lp:X) }} {{ large_int_Neg lp:X }}
           (coqZneg P) :-
   ground-uint X, !,
-  coq.reduction.vm.norm {{ N.succ_pos (N.of_num_uint lp:X) }} {{ positive }} P.
+  coq.reduction.cbv.norm {{ N.succ_pos (N.of_num_uint lp:X) }} P.
 quote.int {{ Negz lp:N }} {{ large_int_Z (Zneg lp:P) }} (coqZneg P) :-
   reduction-pos {{ N.succ_pos (N.of_nat lp:N) }} P, !.
 

diff --git a/theories/ring.elpi b/theories/ring.elpi
@@ -51,7 +51,7 @@ quote.expr.exp In1 In2 {{ @PEpow Z lp:In1 lp:In2 }} :- !.
 pred quote.ncstr i:term, o:term, o:term.
 quote.ncstr {{ Nat.of_num_uint lp:In }} {{ large_nat_uint lp:In }} Out :-
   ground-uint In, !,
-  coq.reduction.vm.norm {{ N.of_num_uint lp:In }} {{ N }} Out.
+  coq.reduction.cbv.norm {{ N.of_num_uint lp:In }} Out.
 quote.ncstr In {{ large_nat_N lp:Out }} Out :-
   reduction-N {{ N.of_nat lp:In }} Out.
 
@@ -60,13 +60,13 @@ pred quote.icstr i:term, o:bool, o:term, o:term.
 quote.icstr {{ Posz (Nat.of_num_uint lp:In) }}
             tt {{ large_nat_uint lp:In }} Out :-
   ground-uint In, !,
-  coq.reduction.vm.norm {{ N.of_num_uint lp:In }} {{ N }} Out.
+  coq.reduction.cbv.norm {{ N.of_num_uint lp:In }} Out.
 quote.icstr {{ Negz (Nat.of_num_uint lp:In) }}
             ff {{ large_nat_uint lp:In }} Out :-
   ground-uint In, !,
-  coq.reduction.vm.norm {{ N.of_num_uint lp:In }} {{ N }} Out.
+  coq.reduction.cbv.norm {{ N.of_num_uint lp:In }} Out.
 quote.icstr In Pos {{ large_nat_N lp:Out }} Out :- !,
-  coq.reduction.vm.norm {{ quote_icstr_helper lp:In }} {{ (bool * N)%type }}
+  coq.reduction.cbv.norm {{ quote_icstr_helper lp:In }}
     {{ (lp:Pos', lp:Out) }}, !,
   ((Pos' = {{ true }}, !, Pos = tt); (Pos' = {{ false }}, !, Pos = ff)), !,
   ground-N Out.
@@ -91,7 +91,7 @@ quote.nat R {{ lib:num.nat.S lp:In }} OutM Out VarMap :- !,
         {quote.expr.constant {{ lib:num.Z.Zpos lp:Out1 }} } Out2 Out).
 quote.nat _ {{ Nat.of_num_uint lp:X }} {{ NC (large_nat_uint lp:X) }} Out _ :-
   ground-uint X, !,
-  coq.reduction.vm.norm {{ Z.of_num_uint lp:X }} {{ Z }} XZ, !,
+  coq.reduction.cbv.norm {{ Z.of_num_uint lp:X }} XZ, !,
   quote.expr.constant XZ Out.
 quote.nat R {{ addn lp:In1 lp:In2 }} {{ NAdd lp:OutM1 lp:OutM2 }} Out VarMap :-
   !,