Merge pull request #109 from Tragicus/mc1256

Lookup abstracted terms using unification
math-comp · Jan 22, 2025 · a9ce79a · a9ce79a
2 parents c819257 + 40fbf43
commit a9ce79a
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 :- 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