Compile with rocq-elpi 3.1.0 (and elpi 3.3.0)

Author: proux01

coq-mathcomp-algebra-tactics.opam

@@ -32,7 +32,7 @@ depends: [
   "coq-mathcomp-ssreflect" {>= "2.4" & < "2.5~" | = "dev"}
   "coq-mathcomp-algebra" 
   "coq-mathcomp-zify" {>= "1.5.0"}
-  "coq-elpi" {>= "2.2.0" & < "3.1~"}
+  "coq-elpi" {>= "2.2.0"}
 ]
 
 tags: [

theories/common.elpi

@@ -11,9 +11,10 @@ mem [Y|_] X 0 :- Y = app [H|_], X = app [H|_], coq.unify-eq X Y ok, !.
 mem [_|XS] X M :- !, mem XS X N, M is N + 1.
 
 % [eucldiv N D M R] N = D * M + R
+:functional
 pred eucldiv o:int, i:int, o:int, i:int.
 eucldiv N D M R :- var N, var M, !, declare_constraint (eucldiv N D M R) [N, M].
-eucldiv N D M R :- var N, N is D * M + R.
+eucldiv N D M R :- var N, !, N is D * M + R.
 eucldiv N D M R :- var M, M is N div D, R is N mod D.
 
 pred positive-constant o:int, o:term.