lookup abstracted terms using unification

math-comp · Jan 22, 2025 · fc1b2ee · fc1b2ee
1 parent c819257
commit fc1b2ee
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/theories/common.elpi b/theories/common.elpi
@@ -7,6 +7,7 @@ list-constant T [X|XS] {{ @cons lp:T lp:X lp:XS' }} :- list-constant T XS XS'.
 
 pred mem o:list term, o:term, o:int.
 mem [X|_] X 0 :- !.
+mem [Y|_] X 0 :- 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